Nuprl Lemma : isaxiom-bool-if-bunion-unit-prod

[t:Unit ⋃ (Top × Top)]. (isaxiom(t) ∈ 𝔹)


Proof




Definitions occuring in Statement :  b-union: A ⋃ B bfalse: ff btrue: tt bool: 𝔹 uall: [x:A]. B[x] top: Top isaxiom: if Ax then otherwise b unit: Unit member: t ∈ T product: x:A × B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  isaxiom_wf_listunion top_wf b-union_wf unit_wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality sqequalRule axiomEquality equalityTransitivity equalitySymmetry productEquality

Latex:
\mforall{}[t:Unit  \mcup{}  (Top  \mtimes{}  Top)].  (isaxiom(t)  \mmember{}  \mBbbB{})



Date html generated: 2016_05_15-PM-10_09_35
Last ObjectModification: 2015_12_27-PM-05_59_17

Theory : eval!all


Home Index