### Nuprl Lemma : id-fun-set

`∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[f:id-fun(A)].  (f ∈ id-fun({a:A| P[a]} ))`

Proof

Definitions occuring in Statement :  id-fun: `id-fun(T)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` so_apply: `x[s]` prop: `ℙ` uimplies: `b supposing a` so_lambda: `λ2x.t[x]`
Lemmas referenced :  id-fun-subtype strong-subtype-set2 id-fun_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesisEquality applyEquality lemma_by_obid sqequalHypSubstitution isectElimination thin setEquality hypothesis lambdaEquality sqequalRule universeEquality independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache functionEquality cumulativity

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[f:id-fun(A)].    (f  \mmember{}  id-fun(\{a:A|  P[a]\}  ))

Date html generated: 2016_05_13-PM-04_12_23
Last ObjectModification: 2015_12_26-AM-11_12_09

Theory : subtype_1

Home Index