### Nuprl Lemma : not-Sierpinski-top

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

Proof

Definitions occuring in Statement :  Sierpinski: `Sierpinski` Sierpinski-top: `⊤` Sierpinski-bottom: `⊥` uall: `∀[x:A]. B[x]` not: `¬A` implies: `P `` Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  iff: `P `⇐⇒` Q` and: `P ∧ Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` Sierpinski: `Sierpinski` quotient: `x,y:A//B[x; y]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` all: `∀x:A. B[x]` prop: `ℙ` rev_implies: `P `` Q` Sierpinski-bottom: `⊥` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` not: `¬A` false: `False` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b`
Lemmas referenced :  Sierpinski-unequal-1 Sierpinski_wf quotient-member-eq nat_wf bool_wf iff_wf equal-wf-T-base two-class-equiv-rel Sierpinski-bottom_wf eqtt_to_assert Sierpinski-top_wf equal-wf-base eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot bfalse_wf not_wf assert_elim btrue_neq_bfalse
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity productElimination thin isect_memberFormation lambdaFormation pointwiseFunctionalityForEquality hypothesis sqequalRule pertypeElimination isectElimination functionEquality lambdaEquality hypothesisEquality baseClosed because_Cache independent_isectElimination dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination independent_pairFormation functionExtensionality rename applyEquality unionElimination equalityElimination voidElimination dependent_pairFormation promote_hyp instantiate cumulativity productEquality axiomEquality applyLambdaEquality

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

Date html generated: 2019_10_31-AM-06_35_29
Last ObjectModification: 2017_07_28-AM-09_11_56

Theory : synthetic!topology

Home Index