---

Step * 1 1 1 of Lemma cantor-theorem-on-power-set


1. T : Type
2. f : T ⟶ T ⟶ 𝔹
3. Inj(T;T ⟶ 𝔹;f)
4. Surj(T;T ⟶ 𝔹;f)
⊢ False
BY
{ ((With ⌜λx.(¬b(f x x))⌝ (D (-1))⋅ THEN Auto) THEN ExRepD) }

1
1. T : Type
2. f : T ⟶ T ⟶ 𝔹
3. Inj(T;T ⟶ 𝔹;f)
4. a : T
5. (f a) = (λx.(¬b(f x x))) ∈ (T ⟶ 𝔹)
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
3.  Inj(T;T  {}\mrightarrow{}  \mBbbB{};f)
4.  Surj(T;T  {}\mrightarrow{}  \mBbbB{};f)
\mvdash{}  False


By

---

Latex:
((With  \mkleeneopen{}\mlambda{}x.(\mneg{}\msubb{}(f  x  x))\mkleeneclose{}  (D  (-1))\mcdot{}  THEN  Auto)  THEN  ExRepD)

---

Home Index