Nuprl Lemma : subtype_rel_list_set

[A,B:Type]. ∀[P:A ⟶ Type]. ∀[Q:B ⟶ Type].
  (({a:A| P[a]}  List) ⊆({b:B| Q[b]}  List)) supposing ((∀x:A. (P[x]  Q[x])) and ({a:A| P[a]}  ⊆B))


Definitions occuring in Statement :  list: List uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] implies:  Q set: {x:A| B[x]}  function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  member: t ∈ T so_apply: x[s] subtype_rel: A ⊆B uall: [x:A]. B[x] uimplies: supposing a so_lambda: λ2x.t[x] prop: implies:  Q
Lemmas referenced :  subtype_rel_list subtype_rel_sets all_wf subtype_rel_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_set_memberEquality hypothesisEquality hypothesis applyEquality sqequalHypSubstitution sqequalRule because_Cache isect_memberFormation introduction lemma_by_obid isectElimination thin setEquality independent_isectElimination lambdaEquality universeEquality axiomEquality cumulativity functionEquality isect_memberEquality equalityTransitivity equalitySymmetry

\mforall{}[A,B:Type].  \mforall{}[P:A  {}\mrightarrow{}  Type].  \mforall{}[Q:B  {}\mrightarrow{}  Type].
    ((\{a:A|  P[a]\}    List)  \msubseteq{}r  (\{b:B|  Q[b]\}    List))  supposing  ((\mforall{}x:A.  (P[x]  {}\mRightarrow{}  Q[x]))  and  (\{a:A|  P[a]\}    \msubseteq{}\000Cr  B))

Date html generated: 2016_05_14-AM-06_25_52
Last ObjectModification: 2015_12_26-PM-00_42_46

Theory : list_0

Home Index