---

Step * of Lemma unary-almost-full-has-strict-inc

∀A:ℕ ⟶ ℙ. ((∀s:StrictInc. ⇃(∃n:ℕ. A[s n])) ⇒ ⇃(∃s:StrictInc. ∀n:ℕ. A[s n]))
BY
{ (Auto THEN Assert ⌜∀m:ℕ. ⇃(∃n:ℕ. (m < n ∧ A[n]))⌝⋅) }

1
.....assertion..... 
1. A : ℕ ⟶ ℙ
2. ∀s:StrictInc. ⇃(∃n:ℕ. A[s n])
⊢ ∀m:ℕ. ⇃(∃n:ℕ. (m < n ∧ A[n]))

2
1. A : ℕ ⟶ ℙ
2. ∀s:StrictInc. ⇃(∃n:ℕ. A[s n])
3. ∀m:ℕ. ⇃(∃n:ℕ. (m < n ∧ A[n]))
⊢ ⇃(∃s:StrictInc. ∀n:ℕ. A[s n])

---

Latex:

---

Latex:
\mforall{}A:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}s:StrictInc.  \00D9(\mexists{}n:\mBbbN{}.  A[s  n]))  {}\mRightarrow{}  \00D9(\mexists{}s:StrictInc.  \mforall{}n:\mBbbN{}.  A[s  n]))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mforall{}m:\mBbbN{}.  \00D9(\mexists{}n:\mBbbN{}.  (m  <  n  \mwedge{}  A[n]))\mkleeneclose{}\mcdot{})

---

Home Index