Metamath Proof Explorer

Theorem peano2nn

Description: Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion peano2nn ⊢ A ∈ ℕ → A + 1 ∈ ℕ

Proof

Step Hyp Ref Expression
1 frfnom ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω Fn ω
2 fvelrnb ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω Fn ω → A ∈ ran ⁡ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ↔ ∃ y ∈ ω rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y = A
3 1 2 ax-mp ⊢ A ∈ ran ⁡ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ↔ ∃ y ∈ ω rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y = A
4 ovex ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y + 1 ∈ V
5 eqid ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω
6 oveq1 ⊢ z = x → z + 1 = x + 1
7 oveq1 ⊢ z = rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y → z + 1 = rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y + 1
8 5 6 7 frsucmpt2 ⊢ y ∈ ω ∧ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y + 1 ∈ V → rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ suc ⁡ y = rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y + 1
9 4 8 mpan2 ⊢ y ∈ ω → rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ suc ⁡ y = rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y + 1
10 peano2 ⊢ y ∈ ω → suc ⁡ y ∈ ω
11 fnfvelrn ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω Fn ω ∧ suc ⁡ y ∈ ω → rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ suc ⁡ y ∈ ran ⁡ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω
12 1 10 11 sylancr ⊢ y ∈ ω → rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ suc ⁡ y ∈ ran ⁡ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω
13 df-nn ⊢ ℕ = rec ⁡ x ∈ V ⟼ x + 1 1 ω
14 df-ima ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ω = ran ⁡ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω
15 13 14 eqtri ⊢ ℕ = ran ⁡ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω
16 12 15 eleqtrrdi ⊢ y ∈ ω → rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ suc ⁡ y ∈ ℕ
17 9 16 eqeltrrd ⊢ y ∈ ω → rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y + 1 ∈ ℕ
18 oveq1 ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y = A → rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y + 1 = A + 1
19 18 eleq1d ⊢ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y = A → rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y + 1 ∈ ℕ ↔ A + 1 ∈ ℕ
20 17 19 syl5ibcom ⊢ y ∈ ω → rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y = A → A + 1 ∈ ℕ
21 20 rexlimiv ⊢ ∃ y ∈ ω rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω ⁡ y = A → A + 1 ∈ ℕ
22 3 21 sylbi ⊢ A ∈ ran ⁡ rec ⁡ x ∈ V ⟼ x + 1 1 ↾ ω → A + 1 ∈ ℕ
23 22 15 eleq2s ⊢ A ∈ ℕ → A + 1 ∈ ℕ