---

Step * 1 of Lemma weakly-infinite-cases


1. S : ℕ ⟶ ℙ
2. w∃∞x.S[x]
3. A : ℕ ⟶ ℙ
4. ∀n:ℕ. (A[n] ⇒ S[n])
5. ¬w∃∞n.A[n]
6. n : ℕ
7. ∀q:ℕ. (¬(n < q ∧ A[q]))
⊢ ¬¬(w∃∞n.A[n] ∨ w∃∞n.S[n] ∧ (¬A[n]))
BY
{ (Assert ⌜w∃∞n.S[n] ∧ (¬A[n])⌝⋅ THEN Auto THEN (D 0 THENA Auto)) }

1
1. S : ℕ ⟶ ℙ
2. w∃∞x.S[x]
3. A : ℕ ⟶ ℙ
4. ∀n:ℕ. (A[n] ⇒ S[n])
5. ¬w∃∞n.A[n]
6. n : ℕ
7. ∀q:ℕ. (¬(n < q ∧ A[q]))
8. n1 : ℕ
⊢ ¬¬(∃q:ℕ. (n1 < q ∧ S[q] ∧ (¬A[q])))

---

Latex:

---

Latex:

1.  S  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  w\mexists{}\minfty{}x.S[x]
3.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}n:\mBbbN{}.  (A[n]  {}\mRightarrow{}  S[n])
5.  \mneg{}w\mexists{}\minfty{}n.A[n]
6.  n  :  \mBbbN{}
7.  \mforall{}q:\mBbbN{}.  (\mneg{}(n  <  q  \mwedge{}  A[q]))
\mvdash{}  \mneg{}\mneg{}(w\mexists{}\minfty{}n.A[n]  \mvee{}  w\mexists{}\minfty{}n.S[n]  \mwedge{}  (\mneg{}A[n]))


By

---

Latex:
(Assert  \mkleeneopen{}w\mexists{}\minfty{}n.S[n]  \mwedge{}  (\mneg{}A[n])\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  (D  0  THENA  Auto))

---

Home Index