Nuprl Lemma : piset_wf

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


Proof




Definitions occuring in Statement :  piset: 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] mk-coset: mk-coset(T;f) piset: piset(A;a.B[a]) subtype_rel: A ⊆B member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  set-item_wf orderedpairset_wf setmem-coset setmem_wf coSet_wf set-dom_wf mk-coset_wf coSet_subtype subtype_coSet
Rules used in proof :  isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality dependent_set_memberEquality dependent_functionElimination universeEquality lambdaEquality because_Cache setEquality functionExtensionality cumulativity functionEquality isectElimination thin productElimination sqequalRule sqequalHypSubstitution applyEquality hypothesisEquality hypothesis extract_by_obid hypothesis_subsumption 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\}].    (piset(A;a.B[a])  \mmember{}  coSet\{i:l\})



Date html generated: 2018_07_29-AM-10_04_22
Last ObjectModification: 2018_07_18-PM-03_27_30

Theory : constructive!set!theory


Home Index