### Nuprl Lemma : Sierpinski-equal2

`∀[x,y:Sierpinski].  uiff(x = y ∈ Sierpinski;x = ⊤ ∈ Sierpinski `⇐⇒` y = ⊤ ∈ Sierpinski)`

Proof

Definitions occuring in Statement :  Sierpinski: `Sierpinski` Sierpinski-top: `⊤` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` iff: `P `⇐⇒` Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` iff: `P `⇐⇒` Q` implies: `P `` Q` prop: `ℙ` rev_implies: `P `` Q` not: `¬A` false: `False`
Lemmas referenced :  equal-wf-T-base Sierpinski_wf equal_wf Sierpinski-equal not-Sierpinski-top Sierpinski-unequal iff_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lambdaFormation equalityTransitivity equalitySymmetry hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality baseClosed because_Cache sqequalRule productElimination independent_pairEquality lambdaEquality dependent_functionElimination axiomEquality independent_isectElimination independent_functionElimination voidElimination isect_memberEquality

Latex:
\mforall{}[x,y:Sierpinski].    uiff(x  =  y;x  =  \mtop{}  \mLeftarrow{}{}\mRightarrow{}  y  =  \mtop{})

Date html generated: 2019_10_31-AM-06_36_29
Last ObjectModification: 2017_07_28-AM-09_12_15

Theory : synthetic!topology

Home Index