Step
*
of Lemma
cantor-theorem-on-power-set
∀[T:Type]. (¬T ~ powerset(T))
BY
{ (Auto THEN Assert ⌜¬T ~ T ⟶ 𝔹⌝⋅) }
1
.....assertion..... 
1. T : Type
⊢ ¬T ~ T ⟶ 𝔹
2
1. T : Type
2. ¬T ~ T ⟶ 𝔹
⊢ ¬T ~ powerset(T)
Latex:
Latex:
\mforall{}[T:Type].  (\mneg{}T  \msim{}  powerset(T))
By
Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mneg{}T  \msim{}  T  {}\mrightarrow{}  \mBbbB{}\mkleeneclose{}\mcdot{})
Home
Index