Nuprl Lemma : Sierpinski-unequal
¬(⊥ = ⊤ ∈ Sierpinski)
Proof
Definitions occuring in Statement :
Sierpinski: Sierpinski,
Sierpinski-top: ⊤,
Sierpinski-bottom: ⊥,
not: ¬A,
equal: s = t ∈ T
Definitions unfolded in proof :
iff: P ⇐⇒ Q,
and: P ∧ Q,
not: ¬A,
implies: P ⇒ Q,
Sierpinski: Sierpinski,
quotient: x,y:A//B[x; y],
false: False,
cand: A c∧ B,
member: t ∈ T,
uall: ∀[x:A]. B[x],
prop: ℙ,
rev_implies: P ⇐ Q,
subtype_rel: A ⊆r B
Lemmas referenced :
Sierpinski-unequal-1,
and_wf,
member_wf,
nat_wf,
bool_wf,
Sierpinski-bottom_wf,
Sierpinski-top_wf,
iff_wf,
equal_wf,
Sierpinski_wf,
subtype-Sierpinski
Rules used in proof :
cut,
lemma_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
productElimination,
thin,
lambdaFormation,
sqequalRule,
pertypeElimination,
independent_functionElimination,
equalityTransitivity,
hypothesis,
equalitySymmetry,
voidElimination,
isectElimination,
functionEquality,
applyEquality
Latex:
\mneg{}(\mbot{} = \mtop{})
Date html generated:
2019_10_31-AM-06_35_32
Last ObjectModification:
2015_12_28-AM-11_22_00
Theory : synthetic!topology
Home
Index