### Nuprl Lemma : strong-subtype-set2

`∀[A:Type]. ∀[P:A ⟶ ℙ].  strong-subtype({x:A| P[x]} ;A)`

Proof

Definitions occuring in Statement :  strong-subtype: `strong-subtype(A;B)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` strong-subtype: `strong-subtype(A;B)` cand: `A c∧ B` subtype_rel: `A ⊆r B` so_apply: `x[s]` exists: `∃x:A. B[x]` and: `P ∧ Q` prop: `ℙ` so_lambda: `λ2x.t[x]` implies: `P `` Q`
Lemmas referenced :  and_wf equal_wf exists_wf strong-subtype_witness
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality setElimination thin rename hypothesisEquality setEquality cumulativity applyEquality functionExtensionality hypothesis because_Cache sqequalHypSubstitution sqequalRule independent_pairFormation productElimination dependent_set_memberEquality equalitySymmetry extract_by_obid isectElimination hyp_replacement Error :applyLambdaEquality,  universeEquality independent_functionElimination functionEquality isect_memberEquality

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].    strong-subtype(\{x:A|  P[x]\}  ;A)

Date html generated: 2016_10_21-AM-09_41_30
Last ObjectModification: 2016_07_12-AM-05_03_32

Theory : subtype_1

Home Index