---

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


1. K : Type
2. K ⊆r ℕ
3. k0 : K
4. CCC(K)
5. CCCNSet(K)
6. L : K List
7. no_repeats(K;L)
8. ∀x:K. (x ∈ L)
9. (k0 ∈ L)
10. 0 < ||L||
11. (imax-list(L) ∈ L)
12. ∀a:ℤ. a ≤ imax-list(L) ⇐⇒ (∃b∈L. a ≤ b) supposing 0 < ||L||
⊢ ∃B:K. ∀k:K. (k ≤ B)
BY
{ (D 0 With ⌜imax-list(L)⌝ 
   THENL [((RepeatFor 2 (D -2) THEN HypSubst' (-2) 0) THEN Auto)
         ; (RWO "-1" 0 THEN Auto THEN (Assert (k ∈ L) BY Auto) THEN D -1 THEN D 0 With ⌜i⌝  THEN Auto)
         ; Auto]
) }

---

Latex:

---

Latex:

1.  K  :  Type
2.  K  \msubseteq{}r  \mBbbN{}
3.  k0  :  K
4.  CCC(K)
5.  CCCNSet(K)
6.  L  :  K  List
7.  no\_repeats(K;L)
8.  \mforall{}x:K.  (x  \mmember{}  L)
9.  (k0  \mmember{}  L)
10.  0  <  ||L||
11.  (imax-list(L)  \mmember{}  L)
12.  \mforall{}a:\mBbbZ{}.  a  \mleq{}  imax-list(L)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}L.  a  \mleq{}  b)  supposing  0  <  ||L||
\mvdash{}  \mexists{}B:K.  \mforall{}k:K.  (k  \mleq{}  B)


By

---

Latex:
(D  0  With  \mkleeneopen{}imax-list(L)\mkleeneclose{} 
  THENL  [((RepeatFor  2  (D  -2)  THEN  HypSubst'  (-2)  0)  THEN  Auto)
              ;  (RWO  "-1"  0  THEN  Auto  THEN  (Assert  (k  \mmember{}  L)  BY  Auto)  THEN  D  -1  THEN  D  0  With  \mkleeneopen{}i\mkleeneclose{}    THEN  Auto)
              ;  Auto]
)

---

Home Index