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