Nuprl Lemma : Sierpinski-cases2

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


Proof




Definitions occuring in Statement :  Sierpinski: Sierpinski Sierpinski-top: Sierpinski-bottom: uall: [x:A]. B[x] not: ¬A or: P ∨ Q equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T not: ¬A implies:  Q and: P ∧ Q cand: c∧ B or: P ∨ Q prop: subtype_rel: A ⊆B guard: {T} false: False
Lemmas referenced :  Sierpinski-cases equal_wf Sierpinski_wf Sierpinski-bottom_wf Sierpinski-top_wf not_wf or_wf subtype-Sierpinski
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation introduction independent_functionElimination inlFormation applyEquality because_Cache sqequalRule independent_pairFormation inrFormation voidElimination

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



Date html generated: 2019_10_31-AM-06_35_36
Last ObjectModification: 2015_12_28-AM-11_21_49

Theory : synthetic!topology


Home Index