---

Step * of Lemma ccc-nset-remove1

∀K:Type. (CCCNSet(K) ⇒ (∀k0,k1:K.  ((¬(k0 = k1 ∈ ℤ)) ⇒ CCCNSet({k:K| ¬(k = k0 ∈ ℤ)} ))))
BY
{ (RepeatFor 2 (Intro)
   THEN RepeatFor 2 (D -1)
   THEN Auto
   THEN D 0
   THEN Auto
   THEN ((UseWitness ⌜k1⌝⋅ THEN Complete (Auto)) ORELSE (D 0 THEN Auto))) }

1
1. K : Type
2. K ⊆r ℕ
3. K
4. CCC(K)
5. k0 : K
6. k1 : K
7. ¬(k0 = k1 ∈ ℤ)
8. {k:K| ¬(k = k0 ∈ ℤ)} 
9. R : ℕ ⟶ {k:K| ¬(k = k0 ∈ ℤ)}  ⟶ ℙ
10. ∀g:ℕ ⟶ {k:K| ¬(k = k0 ∈ ℤ)} . ∃n:ℕ. (R n (g n))
⊢ ∃n:ℕ. ∀m:{k:K| ¬(k = k0 ∈ ℤ)} . (R n m)

---

Latex:

---

Latex:
\mforall{}K:Type.  (CCCNSet(K)  {}\mRightarrow{}  (\mforall{}k0,k1:K.    ((\mneg{}(k0  =  k1))  {}\mRightarrow{}  CCCNSet(\{k:K|  \mneg{}(k  =  k0)\}  ))))


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  RepeatFor  2  (D  -1)
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  ((UseWitness  \mkleeneopen{}k1\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto))  ORELSE  (D  0  THEN  Auto)))

---

Home Index