### Nuprl Lemma : non-axiom-listunion

`∀[A,B:Type]. ∀[L:Unit ⋃ (A × B)].  L ∈ A × B supposing isaxiom(L) = ff`

Proof

Definitions occuring in Statement :  b-union: `A ⋃ B` bfalse: `ff` btrue: `tt` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` isaxiom: `if z = Ax then a otherwise b` unit: `Unit` member: `t ∈ T` product: `x:A × B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` b-union: `A ⋃ B` tunion: `⋃x:A.B[x]` bool: `𝔹` unit: `Unit` ifthenelse: `if b then t else f fi ` pi2: `snd(t)` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ`
Lemmas referenced :  btrue_neq_bfalse equal_wf bool_wf isaxiom_wf_listunion bfalse_wf b-union_wf unit_wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut sqequalHypSubstitution imageElimination productElimination thin unionElimination equalityElimination sqequalRule hypothesis lemma_by_obid independent_functionElimination voidElimination independent_pairEquality hypothesisEquality isectElimination productEquality universeEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:Unit  \mcup{}  (A  \mtimes{}  B)].    L  \mmember{}  A  \mtimes{}  B  supposing  isaxiom(L)  =  ff

Date html generated: 2016_05_14-AM-06_25_12
Last ObjectModification: 2015_12_26-PM-00_42_39

Theory : list_0

Home Index