### Nuprl Lemma : union-product-disjoint

`∀[T,S,A,B:Type].  (¬A + B ⋂ T × S)`

Proof

Definitions occuring in Statement :  isect2: `T1 ⋂ T2` uall: `∀[x:A]. B[x]` not: `¬A` product: `x:A × B[x]` union: `left + right` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` not: `¬A` implies: `P `` Q` false: `False` and: `P ∧ Q` cand: `A c∧ B` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` prop: `ℙ`
Lemmas referenced :  isect2_wf btrue_neq_bfalse isect2_decomp isect2_subtype_rel2 equal_wf btrue_wf isect2_subtype_rel bfalse_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin hypothesis sqequalHypSubstitution independent_functionElimination voidElimination extract_by_obid isectElimination unionEquality cumulativity hypothesisEquality productEquality sqequalRule lambdaEquality dependent_functionElimination because_Cache universeEquality isect_memberEquality rename independent_pairFormation productElimination equalityTransitivity equalitySymmetry applyEquality unionElimination

Latex:
\mforall{}[T,S,A,B:Type].    (\mneg{}A  +  B  \mcap{}  T  \mtimes{}  S)

Date html generated: 2018_05_21-PM-10_19_09
Last ObjectModification: 2017_07_26-PM-06_36_51

Theory : eval!all

Home Index