---

Step * of Lemma ccc-nset-not-not-finite

∀K:Type. (CCCNSet(K) ⇒ (¬¬finite(K)))
BY
{ (InstLemma `ccc-nset-transparent` []
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN D 3
   THEN (D 0 THENA Auto)
   THEN (Assert ∀B:ℕ. ∃k:K. B < k BY
               (ParallelOp -2 THEN D -1 THEN Auto THEN FLemma `bounded-ccc-nset-finite` [-1] THEN Auto))
   THEN (InstLemma `unbounded-ccc-nset-decidable` [⌜K⌝]⋅ THENA Auto)) }

1
1. K : Type
2. CCCNSet(K)
3. K ⊆r ℕ
4. ∀B:ℕ. ((∀k:K. (k ≤ B)) ∨ (∃k:K. B < k))
5. ¬finite(K)
6. ∀B:ℕ. ∃k:K. B < k
7. ∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))
⊢ False

---

Latex:

---

Latex:
\mforall{}K:Type.  (CCCNSet(K)  {}\mRightarrow{}  (\mneg{}\mneg{}finite(K)))


By

---

Latex:
(InstLemma  `ccc-nset-transparent`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  D  3
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  \mforall{}B:\mBbbN{}.  \mexists{}k:K.  B  <  k  BY
                          (ParallelOp  -2
                            THEN  D  -1
                            THEN  Auto
                            THEN  FLemma  `bounded-ccc-nset-finite`  [-1]
                            THEN  Auto))
  THEN  (InstLemma  `unbounded-ccc-nset-decidable`  [\mkleeneopen{}K\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index