# 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}\in ℕ\to {A}+1\in ℕ$

### Proof

Step Hyp Ref Expression
1 frfnom ${⊢}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)Fn\mathrm{\omega }$
2 fvelrnb ${⊢}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)Fn\mathrm{\omega }\to \left({A}\in \mathrm{ran}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)↔\exists {y}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)={A}\right)$
3 1 2 ax-mp ${⊢}{A}\in \mathrm{ran}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)↔\exists {y}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)={A}$
4 ovex ${⊢}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)+1\in \mathrm{V}$
5 eqid ${⊢}{\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}={\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}$
6 oveq1 ${⊢}{z}={x}\to {z}+1={x}+1$
7 oveq1 ${⊢}{z}=\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)\to {z}+1=\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)+1$
8 5 6 7 frsucmpt2 ${⊢}\left({y}\in \mathrm{\omega }\wedge \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)+1\in \mathrm{V}\right)\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{y}\right)=\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)+1$
9 4 8 mpan2 ${⊢}{y}\in \mathrm{\omega }\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{y}\right)=\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)+1$
10 peano2 ${⊢}{y}\in \mathrm{\omega }\to \mathrm{suc}{y}\in \mathrm{\omega }$
11 fnfvelrn ${⊢}\left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)Fn\mathrm{\omega }\wedge \mathrm{suc}{y}\in \mathrm{\omega }\right)\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{y}\right)\in \mathrm{ran}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)$
12 1 10 11 sylancr ${⊢}{y}\in \mathrm{\omega }\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{y}\right)\in \mathrm{ran}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)$
13 df-nn ${⊢}ℕ=\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)\left[\mathrm{\omega }\right]$
14 df-ima ${⊢}\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)\left[\mathrm{\omega }\right]=\mathrm{ran}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)$
15 13 14 eqtri ${⊢}ℕ=\mathrm{ran}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)$
16 12 15 eleqtrrdi ${⊢}{y}\in \mathrm{\omega }\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{y}\right)\in ℕ$
17 9 16 eqeltrrd ${⊢}{y}\in \mathrm{\omega }\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)+1\in ℕ$
18 oveq1 ${⊢}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)={A}\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)+1={A}+1$
19 18 eleq1d ${⊢}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)={A}\to \left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)+1\in ℕ↔{A}+1\in ℕ\right)$
20 17 19 syl5ibcom ${⊢}{y}\in \mathrm{\omega }\to \left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)={A}\to {A}+1\in ℕ\right)$
21 20 rexlimiv ${⊢}\exists {y}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)={A}\to {A}+1\in ℕ$
22 3 21 sylbi ${⊢}{A}\in \mathrm{ran}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\to {A}+1\in ℕ$
23 22 15 eleq2s ${⊢}{A}\in ℕ\to {A}+1\in ℕ$