Nuprl Lemma : sp-join-idemp

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


Proof




Definitions occuring in Statement :  sp-join: f ∨ g Sierpinski: Sierpinski uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a iff: ⇐⇒ Q implies:  Q prop: rev_implies:  Q
Lemmas referenced :  Sierpinski-equal sp-join_wf Sierpinski_wf equal-wf-T-base iff_wf sp-join-is-bottom
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis productElimination independent_isectElimination independent_pairFormation lambdaFormation productEquality baseClosed because_Cache addLevel impliesFunctionality independent_functionElimination

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



Date html generated: 2019_10_31-AM-07_18_39
Last ObjectModification: 2017_07_28-AM-09_12_21

Theory : synthetic!topology


Home Index