---

Step * 1 1 1 1 2 2 1 of Lemma CCC-omni


1. K : Type
2. K ⊆r ℕ
3. k : 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. g : ℕ ⟶ K
11. ¬P[g k]
12. ¬(∀k@0:K. ((k@0 ≤ (g k)) ⇒ (¬P[k@0])))
13. Dec(∃k@0:K. ((k@0 ≤ (g k)) ∧ P[k@0]))
⊢ ∃n:ℕ. ((n ∈ K) ∧ ((∃k:K. ((k ≤ n) ∧ P[k])) ∨ (∀k:K. ((k ≤ (g n)) ⇒ (¬P[k])))))
BY
{ D -1 }

1
1. K : Type
2. K ⊆r ℕ
3. k : 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. g : ℕ ⟶ K
11. ¬P[g k]
12. ¬(∀k@0:K. ((k@0 ≤ (g k)) ⇒ (¬P[k@0])))
13. ∃k@0:K. ((k@0 ≤ (g k)) ∧ P[k@0])
⊢ ∃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 : 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. g : ℕ ⟶ K
11. ¬P[g k]
12. ¬(∀k@0:K. ((k@0 ≤ (g k)) ⇒ (¬P[k@0])))
13. ¬(∃k@0:K. ((k@0 ≤ (g k)) ∧ P[k@0]))
⊢ ∃n:ℕ. ((n ∈ K) ∧ ((∃k:K. ((k ≤ n) ∧ P[k])) ∨ (∀k:K. ((k ≤ (g n)) ⇒ (¬P[k])))))

---

Latex:

---

Latex:

1.  K  :  Type
2.  K  \msubseteq{}r  \mBbbN{}
3.  k  :  K
4.  P  :  K  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}k:K.  Dec(P[k])
6.  WD(K)
7.  \mexists{}n:K.  \mforall{}m:K.  (n  \mleq{}  m)
8.  \mforall{}n:K.  \mforall{}k:\mBbbN{}n  +  1.    Dec(k  \mmember{}  K)
9.  \mforall{}n:K.  Dec(\mforall{}k:K.  ((k  \mleq{}  n)  {}\mRightarrow{}  (\mneg{}P[k])))
10.  g  :  \mBbbN{}  {}\mrightarrow{}  K
11.  \mneg{}P[g  k]
12.  \mneg{}(\mforall{}k@0:K.  ((k@0  \mleq{}  (g  k))  {}\mRightarrow{}  (\mneg{}P[k@0])))
13.  Dec(\mexists{}k@0:K.  ((k@0  \mleq{}  (g  k))  \mwedge{}  P[k@0]))
\mvdash{}  \mexists{}n:\mBbbN{}.  ((n  \mmember{}  K)  \mwedge{}  ((\mexists{}k:K.  ((k  \mleq{}  n)  \mwedge{}  P[k]))  \mvee{}  (\mforall{}k:K.  ((k  \mleq{}  (g  n))  {}\mRightarrow{}  (\mneg{}P[k])))))


By

---

Latex:
D  -1

---

Home Index