### Nuprl Lemma : product-unit-disjoint

`∀[T,S:Type].  (¬T × S ⋂ Unit)`

Proof

Definitions occuring in Statement :  isect2: `T1 ⋂ T2` uall: `∀[x:A]. B[x]` not: `¬A` unit: `Unit` product: `x:A × B[x]` 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: `ℙ` unit: `Unit`
Lemmas referenced :  btrue_neq_bfalse isect2_wf unit_wf2 isect2_decomp isect2_subtype_rel btrue_wf equal_wf isect2_subtype_rel2 bfalse_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin rename independent_pairFormation hypothesis sqequalHypSubstitution productElimination equalityTransitivity equalitySymmetry extract_by_obid independent_functionElimination voidElimination because_Cache isectElimination productEquality cumulativity hypothesisEquality sqequalRule lambdaEquality dependent_functionElimination universeEquality isect_memberEquality applyEquality equalityElimination

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

Date html generated: 2018_05_21-PM-10_19_05
Last ObjectModification: 2017_07_26-PM-06_36_50

Theory : eval!all

Home Index