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: A c∧ B
, 
guard: {T}
, 
so_apply: x[s]
, 
so_lambda: λ2x.t[x]
, 
implies: P 
⇒ Q
, 
rev_implies: P 
⇐ Q
, 
and: P ∧ Q
, 
iff: P 
⇐⇒ 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