---

Step * 1 1 1 1 of Lemma weakly-infinite-cases


1. S : ℕ ⟶ ℙ
2. A : ℕ ⟶ ℙ
3. ∀n:ℕ. (A[n] ⇒ S[n])
4. ¬w∃∞n.A[n]
5. n : ℕ
6. ∀q:ℕ. (¬(n < q ∧ A[q]))
7. n1 : ℕ
8. m : ℕ
9. n ≤ m
10. n1 ≤ m
11. q : ℕ
12. m < q
13. S[q]
14. S[q]
⊢ ¬A[q]
BY
{ (InstHyp [⌜q⌝] 6⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  S  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}n:\mBbbN{}.  (A[n]  {}\mRightarrow{}  S[n])
4.  \mneg{}w\mexists{}\minfty{}n.A[n]
5.  n  :  \mBbbN{}
6.  \mforall{}q:\mBbbN{}.  (\mneg{}(n  <  q  \mwedge{}  A[q]))
7.  n1  :  \mBbbN{}
8.  m  :  \mBbbN{}
9.  n  \mleq{}  m
10.  n1  \mleq{}  m
11.  q  :  \mBbbN{}
12.  m  <  q
13.  S[q]
14.  S[q]
\mvdash{}  \mneg{}A[q]


By

---

Latex:
(InstHyp  [\mkleeneopen{}q\mkleeneclose{}]  6\mcdot{}  THEN  Auto)

---

Home Index