### Nuprl Lemma : Russell-theorem-take2

`¬(Type ∈ Type)`

Proof

Definitions occuring in Statement :  not: `¬A` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  not: `¬A` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` guard: `{T}` isect2: `T1 ⋂ T2` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` and: `P ∧ Q` cand: `A c∧ B` squash: `↓T` false: `False`
Lemmas referenced :  isect2_decomp bool_wf isect2_subtype_rel2 isect2_subtype_rel not_wf base_wf isect2_wf equal-wf-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalRule cut instantiate lemma_by_obid sqequalHypSubstitution isectElimination thin universeEquality baseClosed because_Cache hypothesis hypothesisEquality applyEquality cumulativity equalityTransitivity equalitySymmetry isect_memberEquality unionElimination equalityElimination setEquality dependent_functionElimination productElimination independent_pairFormation lambdaEquality setElimination rename imageMemberEquality introduction imageElimination independent_functionElimination voidElimination dependent_set_memberEquality

Latex:
\mneg{}(Type  \mmember{}  Type)

Date html generated: 2016_05_15-PM-01_44_06
Last ObjectModification: 2016_01_15-PM-11_17_40

Theory : basic

Home Index