Nuprl Lemma : Piset_wf

[A:coSet{i:l}]. ∀[B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}].  a:A.B[a] ∈ coSet{i:l})


Proof




Definitions occuring in Statement :  Piset: Πa:A.B[a] setmem: (x ∈ s) coSet: coSet{i:l} uall: [x:A]. B[x] so_apply: x[s] member: t ∈ T set: {x:A| B[x]}  function: x:A ⟶ B[x]
Definitions unfolded in proof :  all: x:A. B[x] prop: so_apply: x[s] so_lambda: λ2x.t[x] Piset: Πa:A.B[a] member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  singlevalued-graph_wf setmem_wf coSet_wf piset_wf sub-set_wf
Rules used in proof :  because_Cache isect_memberEquality functionEquality equalitySymmetry equalityTransitivity axiomEquality rename setElimination dependent_functionElimination cumulativity hypothesis setEquality applyEquality lambdaEquality hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[A:coSet\{i:l\}].  \mforall{}[B:\{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  coSet\{i:l\}].    (\mPi{}a:A.B[a]  \mmember{}  coSet\{i:l\})



Date html generated: 2018_07_29-AM-10_05_04
Last ObjectModification: 2018_07_18-PM-03_32_46

Theory : constructive!set!theory


Home Index