Nuprl Lemma : setTC_functionality
∀a,b:Set{i:l}. (seteq(a;b) ⇒ seteq(setTC(a);setTC(b)))
Proof
Definitions occuring in Statement :
setTC: setTC(a),
seteq: seteq(s1;s2),
Set: Set{i:l},
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
cand: A c∧ B,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
setTC_functionality_subset,
setsubset_wf,
Set_wf,
seteq-iff-setsubset,
setTC_wf,
seteq_wf,
all_wf
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
introduction,
extract_by_obid,
dependent_functionElimination,
hypothesisEquality,
independent_functionElimination,
hypothesis,
independent_pairFormation,
productEquality,
isectElimination,
addLevel,
allFunctionality,
impliesFunctionality,
cumulativity,
instantiate,
sqequalRule,
lambdaEquality,
functionEquality
Latex:
\mforall{}a,b:Set\{i:l\}. (seteq(a;b) {}\mRightarrow{} seteq(setTC(a);setTC(b)))
Date html generated:
2018_05_22-PM-09_51_23
Last ObjectModification:
2018_05_22-AM-10_53_37
Theory : constructive!set!theory
Home
Index