---

Step * of Lemma not-d-CCC-infinite

∀[A:Type]. ((∃f:A ⟶ ℕ. Surj(A;ℕ;f)) ⇒ (¬dCCC(A)))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN FLemma `d-CCC-surjection` [-1;-2]
   THEN Auto
   THEN MoveToConcl (-1)
   THEN Fold `not` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  ((\mexists{}f:A  {}\mrightarrow{}  \mBbbN{}.  Surj(A;\mBbbN{};f))  {}\mRightarrow{}  (\mneg{}dCCC(A)))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  FLemma  `d-CCC-surjection`  [-1;-2]
  THEN  Auto
  THEN  MoveToConcl  (-1)
  THEN  Fold  `not`  0
  THEN  Auto)

---

Home Index