Step
*
1
of Lemma
Russell-paradox
1. 𝕌' ⊆r Type
⊢ Russell ∈ Russell
BY
{ TACTIC:MemTypeCD }
1
1. 𝕌' ⊆r Type
⊢ Russell ∈ Type ⋂ Base
2
.....set predicate..... 
1. 𝕌' ⊆r Type
⊢ ¬(Russell ∈ Russell)
3
.....wf..... 
1. 𝕌' ⊆r Type
2. T : Type ⋂ Base
⊢ istype(¬(T ∈ T))
Latex:
Latex:
1.  \mBbbU{}'  \msubseteq{}r  Type
\mvdash{}  Russell  \mmember{}  Russell
By
Latex:
TACTIC:MemTypeCD
Home
Index