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:  Q equal: t ∈ T
Definitions unfolded in proof :  iff: ⇐⇒ Q and: P ∧ Q uall: [x:A]. B[x] member: t ∈ T implies:  Q Sierpinski: Sierpinski quotient: x,y:A//B[x; y] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a all: x:A. B[x] prop: rev_implies:  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 then else 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