---

Step * 1 1 of Lemma CCC-omni


1. K : Type
2. CCCNSet(K)
3. P : K ⟶ ℙ
4. ∀k:K. Dec(P[k])
5. WD(K)
6. ∃n:K. ∀m:K. (n ≤ m)
7. ∀n:K. ∀k:ℕn + 1.  Dec(k ∈ K)
8. ∀n:K. Dec(∃k:K. ((k ≤ n) ∧ P[k]))
9. ∀n:K. Dec(∀k:K. ((k ≤ n) ⇒ (¬P[k])))
⊢ (∃k:K. P[k]) ∨ (∀k:K. (¬P[k]))
BY
{ (D 2
   THEN D 3
   THEN (D 4 With ⌜λn,m. ((n ∈ K) ∧ ((∃k:K. ((k ≤ n) ∧ P[k])) ∨ (∀k:K. ((k ≤ m) ⇒ (¬P[k])))))⌝  THENA Auto)
   THEN Reduce -1
   THEN D -1) }

1
.....antecedent..... 
1. K : Type
2. K ⊆r ℕ
3. K
4. P : K ⟶ ℙ
5. ∀k:K. Dec(P[k])
6. WD(K)
7. ∃n:K. ∀m:K. (n ≤ m)
8. ∀n:K. ∀k:ℕn + 1.  Dec(k ∈ K)
9. ∀n:K. Dec(∃k:K. ((k ≤ n) ∧ P[k]))
10. ∀n:K. Dec(∀k:K. ((k ≤ n) ⇒ (¬P[k])))
⊢ ∀g:ℕ ⟶ K. ∃n:ℕ. ((n ∈ K) ∧ ((∃k:K. ((k ≤ n) ∧ P[k])) ∨ (∀k:K. ((k ≤ (g n)) ⇒ (¬P[k])))))

2
1. K : Type
2. K ⊆r ℕ
3. K
4. P : K ⟶ ℙ
5. ∀k:K. Dec(P[k])
6. WD(K)
7. ∃n:K. ∀m:K. (n ≤ m)
8. ∀n:K. ∀k:ℕn + 1.  Dec(k ∈ K)
9. ∀n:K. Dec(∃k:K. ((k ≤ n) ∧ P[k]))
10. ∀n:K. Dec(∀k:K. ((k ≤ n) ⇒ (¬P[k])))
11. ∃n:ℕ. ∀m:K. ((n ∈ K) ∧ ((∃k:K. ((k ≤ n) ∧ P[k])) ∨ (∀k:K. ((k ≤ m) ⇒ (¬P[k])))))
⊢ (∃k:K. P[k]) ∨ (∀k:K. (¬P[k]))

---

Latex:

---

Latex:

1.  K  :  Type
2.  CCCNSet(K)
3.  P  :  K  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}k:K.  Dec(P[k])
5.  WD(K)
6.  \mexists{}n:K.  \mforall{}m:K.  (n  \mleq{}  m)
7.  \mforall{}n:K.  \mforall{}k:\mBbbN{}n  +  1.    Dec(k  \mmember{}  K)
8.  \mforall{}n:K.  Dec(\mexists{}k:K.  ((k  \mleq{}  n)  \mwedge{}  P[k]))
9.  \mforall{}n:K.  Dec(\mforall{}k:K.  ((k  \mleq{}  n)  {}\mRightarrow{}  (\mneg{}P[k])))
\mvdash{}  (\mexists{}k:K.  P[k])  \mvee{}  (\mforall{}k:K.  (\mneg{}P[k]))


By

---

Latex:
(D  2
  THEN  D  3
  THEN  (D  4  With  \mkleeneopen{}\mlambda{}n,m.  ((n  \mmember{}  K)  \mwedge{}  ((\mexists{}k:K.  ((k  \mleq{}  n)  \mwedge{}  P[k]))  \mvee{}  (\mforall{}k:K.  ((k  \mleq{}  m)  {}\mRightarrow{}  (\mneg{}P[k])))))\mkleeneclose{} 
              THENA  Auto
              )
  THEN  Reduce  -1
  THEN  D  -1)

---

Home Index