Nuprl Lemma : set-eq_wf
∀[s,s':coSet{i:l}]. (set-eq(s;s') ∈ ℙ)
Proof
Definitions occuring in Statement :
set-eq: set-eq(s;s'),
coSet: coSet{i:l},
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
set-eq: set-eq(s;s'),
so_lambda: λ2x.t[x],
prop: ℙ,
and: P ∧ Q,
so_apply: x[s],
exists: ∃x:A. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q
Lemmas referenced :
bigrel_wf,
coSet_wf,
all_wf,
set-dom_wf,
exists_wf,
set-item_wf,
equal_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
lambdaEquality,
productEquality,
hypothesisEquality,
applyEquality,
functionEquality,
universeEquality,
lambdaFormation,
instantiate,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
axiomEquality,
isect_memberEquality,
because_Cache
Latex:
\mforall{}[s,s':coSet\{i:l\}]. (set-eq(s;s') \mmember{} \mBbbP{})
Date html generated:
2019_10_31-AM-06_32_44
Last ObjectModification:
2018_08_04-PM-05_18_05
Theory : constructive!set!theory
Home
Index