---

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