---

Step * of Lemma ccc-nset-iff-finite

∀K:Type. ((K ⊆r ℕ) ⇒ K ⇒ (CCC(K) ⇐⇒ finite(K)))
BY
{ (EAuto 1
   THEN (Assert CCCNSet(K) BY
               (D 0 THEN Auto))
   THEN (Assert ⌜∃B:ℕ. ∀k:K. (k ≤ B)⌝⋅ THENM (D -1 THEN InstLemma `bounded-ccc-nset-finite` [⌜K⌝;⌜B⌝]⋅ THEN Auto))
   THEN (Assert ¬¬(∃B:K. ∀k:K. (k ≤ B)) BY
               ((InstLemma `ccc-nset-not-not-finite` [⌜K⌝]⋅ THENA Auto) THEN RepeatFor 2 (ParallelLast)))) }

1
.....aux..... 
1. K : Type
2. K ⊆r ℕ
3. K
4. CCC(K)
5. CCCNSet(K)
6. finite(K)
⊢ ∃B:K. ∀k:K. (k ≤ B)

2
1. K : Type
2. K ⊆r ℕ
3. K
4. CCC(K)
5. CCCNSet(K)
6. ¬¬(∃B:K. ∀k:K. (k ≤ B))
⊢ ∃B:ℕ. ∀k:K. (k ≤ B)

---

Latex:

---

Latex:
\mforall{}K:Type.  ((K  \msubseteq{}r  \mBbbN{})  {}\mRightarrow{}  K  {}\mRightarrow{}  (CCC(K)  \mLeftarrow{}{}\mRightarrow{}  finite(K)))


By

---

Latex:
(EAuto  1
  THEN  (Assert  CCCNSet(K)  BY
                          (D  0  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}\mexists{}B:\mBbbN{}.  \mforall{}k:K.  (k  \mleq{}  B)\mkleeneclose{}\mcdot{}
  THENM  (D  -1  THEN  InstLemma  `bounded-ccc-nset-finite`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THEN  Auto)
  )
  THEN  (Assert  \mneg{}\mneg{}(\mexists{}B:K.  \mforall{}k:K.  (k  \mleq{}  B))  BY
                          ((InstLemma  `ccc-nset-not-not-finite`  [\mkleeneopen{}K\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  RepeatFor  2  (ParallelLast)
                            )))

---

Home Index