---

Step * of Lemma d-CCC-surjection

∀[A,B:Type].  ((∃f:A ⟶ B. Surj(A;B;f)) ⇒ dCCC(A) ⇒ dCCC(B))
BY
{ (Auto
   THEN ExRepD
   THEN ParallelLast
   THEN Auto
   THEN (D -3 With ⌜λn,a. (R n (f a))⌝  THENA Auto)
   THEN Reduce -1
   THEN (D -1 THENA (Auto THEN (D -2 With ⌜f o g⌝  THENA Auto) THEN Reduce -1 THEN Auto))) }

1
1. [A] : Type
2. [B] : Type
3. f : A ⟶ B
4. Surj(A;B;f)
5. R : ℕ ⟶ B ⟶ 𝔹
6. ∀g:ℕ ⟶ B. ∃n:ℕ. (↑(R n (g n)))
7. ∃n:ℕ. ∀m:A. (↑(R n (f m)))
⊢ ∃n:ℕ. ∀m:B. (↑(R n m))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  ParallelLast
  THEN  Auto
  THEN  (D  -3  With  \mkleeneopen{}\mlambda{}n,a.  (R  n  (f  a))\mkleeneclose{}    THENA  Auto)
  THEN  Reduce  -1
  THEN  (D  -1  THENA  (Auto  THEN  (D  -2  With  \mkleeneopen{}f  o  g\mkleeneclose{}    THENA  Auto)  THEN  Reduce  -1  THEN  Auto)))

---

Home Index