### Nuprl Lemma : subtype_rel_nested_set

[A,B:Type]. ∀[P:B ⟶ ℙ]. ∀[Q:{b:B| P[b]}  ⟶ ℙ].  A ⊆{b:{b:B| P[b]} Q[b]}  supposing A ⊆{b:B| P[b] ∧ Q[b]}

Proof

Definitions occuring in Statement :  uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] prop: so_apply: x[s] and: P ∧ Q set: {x:A| B[x]}  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 and: P ∧ Q so_apply: x[s] prop:
Lemmas referenced :  subtype_rel_wf subtype_rel_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule axiomEquality hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality setEquality productEquality applyEquality because_Cache dependent_set_memberEquality isect_memberEquality equalityTransitivity equalitySymmetry functionEquality universeEquality lambdaEquality independent_isectElimination setElimination rename productElimination

Latex:
\mforall{}[A,B:Type].  \mforall{}[P:B  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q:\{b:B|  P[b]\}    {}\mrightarrow{}  \mBbbP{}].
A  \msubseteq{}r  \{b:\{b:B|  P[b]\}  |  Q[b]\}    supposing  A  \msubseteq{}r  \{b:B|  P[b]  \mwedge{}  Q[b]\}

Date html generated: 2016_05_13-PM-03_18_49
Last ObjectModification: 2015_12_26-AM-09_08_22

Theory : subtype_0

Home Index