Step
*
2
1
1
of Lemma
unary-almost-full-has-strict-inc
1. A : ℕ ⟶ ℙ
2. ∀s:StrictInc. ⇃(∃n:ℕ. A[s n])
3. ∀m:ℕ. ⇃(∃n:ℕ. (m < n ∧ A[n]))
4. ∃f:ℕ ⟶ ℕ. ∀n:ℕ. (n < f n ∧ A[f n])
⊢ ∃s:StrictInc. ∀n:ℕ. A[s n]
BY
{ (ExRepD THEN RenameVar `F' (-2)) }
1
1. A : ℕ ⟶ ℙ
2. ∀s:StrictInc. ⇃(∃n:ℕ. A[s n])
3. ∀m:ℕ. ⇃(∃n:ℕ. (m < n ∧ A[n]))
4. F : ℕ ⟶ ℕ
5. ∀n:ℕ. (n < F n ∧ A[F n])
⊢ ∃s:StrictInc. ∀n:ℕ. A[s n]
Latex:
Latex:
1. A : \mBbbN{} {}\mrightarrow{} \mBbbP{}
2. \mforall{}s:StrictInc. \00D9(\mexists{}n:\mBbbN{}. A[s n])
3. \mforall{}m:\mBbbN{}. \00D9(\mexists{}n:\mBbbN{}. (m < n \mwedge{} A[n]))
4. \mexists{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \mforall{}n:\mBbbN{}. (n < f n \mwedge{} A[f n])
\mvdash{} \mexists{}s:StrictInc. \mforall{}n:\mBbbN{}. A[s n]
By
Latex:
(ExRepD THEN RenameVar `F' (-2))
Home
Index