---

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

∀[T:Type]. ∀f:T ⟶ T ⟶ ℙ. ∃P:T ⟶ ℙ. ∀x:T. (¬(∀y:T. (P y ⇐⇒ f x y)))
BY
{ (Auto THEN With ⌜λx.(¬(f x x))⌝ (D 0)⋅ THEN Auto THEN Reduce 0 THEN D 0 THEN Auto) }

1
1. T : Type
2. f : T ⟶ T ⟶ ℙ
3. x : T
4. ∀y:T. (¬(f y y) ⇐⇒ f x y)
⊢ False

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}f:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mexists{}P:T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}x:T.  (\mneg{}(\mforall{}y:T.  (P  y  \mLeftarrow{}{}\mRightarrow{}  f  x  y)))


By

---

Latex:
(Auto  THEN  With  \mkleeneopen{}\mlambda{}x.(\mneg{}(f  x  x))\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  Reduce  0  THEN  D  0  THEN  Auto)

---

Home Index