Nuprl Lemma : subtype_rel_sets

[A,B:Type]. ∀[P:A ⟶ ℙ]. ∀[Q:B ⟶ ℙ].  ({a:A| P[a]}  ⊆{b:B| Q[b]} supposing ((∀a:A. (P[a]  Q[a])) and ({a:A| P[a]\000C}  ⊆B))


Proof




Definitions occuring in Statement :  uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] prop: 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 prop: so_lambda: λ2x.t[x] implies:  Q guard: {T} all: x:A. B[x]
Lemmas referenced :  all_wf subtype_rel_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_set_memberEquality hypothesisEquality hypothesis applyEquality thin because_Cache sqequalHypSubstitution sqequalRule isect_memberFormation introduction axiomEquality lemma_by_obid isectElimination cumulativity lambdaEquality functionEquality universeEquality isect_memberEquality equalityTransitivity equalitySymmetry setEquality setElimination rename dependent_functionElimination independent_functionElimination

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



Date html generated: 2016_05_13-PM-03_18_47
Last ObjectModification: 2015_12_26-AM-09_08_29

Theory : subtype_0


Home Index