---

Step * 1 of Lemma not-CCC-infinite


1. A : Type
2. ∃f:A ⟶ ℕ. Surj(A;ℕ;f)
3. CCC(A)
4. R : ℕ ⟶ A ⟶ 𝔹
5. ∀g:ℕ ⟶ A. ∃n:ℕ. (↑(R n (g n)))
⊢ ∃n:ℕ. ∀m:A. (↑(R n m))
BY
{ (D 3 With ⌜λn,m. (↑(R n m))⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  \mexists{}f:A  {}\mrightarrow{}  \mBbbN{}.  Surj(A;\mBbbN{};f)
3.  CCC(A)
4.  R  :  \mBbbN{}  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}
5.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  A.  \mexists{}n:\mBbbN{}.  (\muparrow{}(R  n  (g  n)))
\mvdash{}  \mexists{}n:\mBbbN{}.  \mforall{}m:A.  (\muparrow{}(R  n  m))


By

---

Latex:
(D  3  With  \mkleeneopen{}\mlambda{}n,m.  (\muparrow{}(R  n  m))\mkleeneclose{}    THEN  Auto)

---

Home Index