Nuprl Lemma : orderedpair-first

a,b:coSet{i:l}.  seteq(orderedpair-fsts((a,b));{a})


Proof




Definitions occuring in Statement :  orderedpair-fsts: orderedpair-fsts(pr) orderedpairset: (a,b) singleset: {a} seteq: seteq(s1;s2) coSet: coSet{i:l} all: x:A. B[x]
Definitions unfolded in proof :  cand: c∧ B guard: {T} so_apply: x[s] so_lambda: λ2x.t[x] implies:  Q rev_implies:  Q and: P ∧ Q iff: ⇐⇒ Q or: P ∨ Q prop: orderedpairset: (a,b) uall: [x:A]. B[x] exists: x:A. B[x] member: t ∈ T all: x:A. B[x] orderedpair-fsts: orderedpair-fsts(pr)
Lemmas referenced :  seteq-iff-setsubset seteq_weakening setmem_functionality setmem-intersectionset all_wf or_wf intersectionset_wf setsubset-iff setmem-pairset iff_wf setmem-singleset seteq_wf co-seteq-iff pairset_wf orderedpairset_wf setmem_wf singleset_wf coSet_wf
Rules used in proof :  impliesLevelFunctionality allLevelFunctionality unionElimination functionEquality lambdaEquality instantiate cumulativity allFunctionality impliesFunctionality addLevel independent_pairFormation independent_functionElimination productElimination dependent_functionElimination inlFormation because_Cache hypothesisEquality thin isectElimination sqequalHypSubstitution dependent_pairFormation hypothesis extract_by_obid introduction cut lambdaFormation computationStep sqequalTransitivity sqequalReflexivity sqequalRule sqequalSubstitution

Latex:
\mforall{}a,b:coSet\{i:l\}.    seteq(orderedpair-fsts((a,b));\{a\})



Date html generated: 2018_07_29-AM-10_01_58
Last ObjectModification: 2018_07_18-PM-03_00_42

Theory : constructive!set!theory


Home Index