Nuprl Lemma : sp-join-top

[x:Sierpinski]. (x ∨ ⊤ = ⊤ ∈ Sierpinski)


Proof




Definitions occuring in Statement :  sp-join: f ∨ g Sierpinski: Sierpinski Sierpinski-top: uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a iff: ⇐⇒ Q implies:  Q prop: rev_implies:  Q cand: c∧ B not: ¬A false: False
Lemmas referenced :  Sierpinski-equal sp-join_wf Sierpinski-top_wf subtype-Sierpinski sp-join-is-bottom equal_wf Sierpinski_wf Sierpinski-bottom_wf Sierpinski-unequal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality sqequalRule because_Cache productElimination independent_isectElimination independent_pairFormation lambdaFormation independent_functionElimination equalitySymmetry voidElimination

Latex:
\mforall{}[x:Sierpinski].  (x  \mvee{}  \mtop{}  =  \mtop{})



Date html generated: 2019_10_31-AM-06_36_45
Last ObjectModification: 2015_12_28-AM-11_20_50

Theory : synthetic!topology


Home Index