---

Step * 2 of Lemma ccc-nset-iff-finite


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)
BY
{ (FLemma `CCC-Sigma02-dns` [-1] THEN Auto THEN ParallelLast) }

---

Latex:

---

Latex:

1.  K  :  Type
2.  K  \msubseteq{}r  \mBbbN{}
3.  K
4.  CCC(K)
5.  CCCNSet(K)
6.  \mneg{}\mneg{}(\mexists{}B:K.  \mforall{}k:K.  (k  \mleq{}  B))
\mvdash{}  \mexists{}B:\mBbbN{}.  \mforall{}k:K.  (k  \mleq{}  B)


By

---

Latex:
(FLemma  `CCC-Sigma02-dns`  [-1]  THEN  Auto  THEN  ParallelLast)

---

Home Index