Nuprl Lemma : sq_exists_subtype_rel

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


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] sq_exists: x:{A| B[x]} implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a subtype_rel: A ⊆B sq_exists: x:{A| B[x]} so_lambda: λ2x.t[x] so_apply: x[s] guard: {T} prop: implies:  Q
Lemmas referenced :  subtype_rel_sets subtype_rel_transitivity sq_exists_wf all_wf subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality sqequalHypSubstitution hypothesisEquality applyEquality lemma_by_obid isectElimination thin because_Cache sqequalRule independent_isectElimination hypothesis axiomEquality functionEquality isect_memberEquality equalityTransitivity equalitySymmetry cumulativity universeEquality

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

Date html generated: 2016_05_15-PM-06_37_53
Last ObjectModification: 2015_12_27-AM-11_54_12

Theory : general

Home Index