---

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


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
BY
{ (Assert ⌜f a a = (λx.(¬b(f x x))) a⌝⋅ THEN Auto THEN Reduce (-1)) }

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 ⟶ 𝔹)
6. f a a = ¬b(f a a)
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
3.  Inj(T;T  {}\mrightarrow{}  \mBbbB{};f)
4.  a  :  T
5.  (f  a)  =  (\mlambda{}x.(\mneg{}\msubb{}(f  x  x)))
\mvdash{}  False


By

---

Latex:
(Assert  \mkleeneopen{}f  a  a  =  (\mlambda{}x.(\mneg{}\msubb{}(f  x  x)))  a\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  Reduce  (-1))

---

Home Index