# Metamath Proof Explorer

## Theorem peano5nni

Description: Peano's inductive postulate. Theorem I.36 (principle of mathematical induction) of Apostol p. 34. (Contributed by NM, 10-Jan-1997) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion peano5nni ${⊢}\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\to ℕ\subseteq {A}$

### Proof

Step Hyp Ref Expression
1 df-nn ${⊢}ℕ=\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)\left[\mathrm{\omega }\right]$
2 df-ima ${⊢}\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)\left[\mathrm{\omega }\right]=\mathrm{ran}\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)$
3 1 2 eqtri ${⊢}ℕ=\mathrm{ran}\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)$
4 frfnom ${⊢}\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)Fn\mathrm{\omega }$
5 4 a1i ${⊢}\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)Fn\mathrm{\omega }$
6 fveq2 ${⊢}{y}=\varnothing \to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)=\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\varnothing \right)$
7 6 eleq1d ${⊢}{y}=\varnothing \to \left(\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)\in {A}↔\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\varnothing \right)\in {A}\right)$
8 fveq2 ${⊢}{y}={z}\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)=\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)$
9 8 eleq1d ${⊢}{y}={z}\to \left(\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)\in {A}↔\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)\in {A}\right)$
10 fveq2 ${⊢}{y}=\mathrm{suc}{z}\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)=\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{z}\right)$
11 10 eleq1d ${⊢}{y}=\mathrm{suc}{z}\to \left(\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)\in {A}↔\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{z}\right)\in {A}\right)$
12 ax-1cn ${⊢}1\in ℂ$
13 fr0g ${⊢}1\in ℂ\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\varnothing \right)=1$
14 12 13 ax-mp ${⊢}\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\varnothing \right)=1$
15 simpl ${⊢}\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\to 1\in {A}$
16 14 15 eqeltrid ${⊢}\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\varnothing \right)\in {A}$
17 oveq1 ${⊢}{x}=\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)\to {x}+1=\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)+1$
18 17 eleq1d ${⊢}{x}=\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)\to \left({x}+1\in {A}↔\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)+1\in {A}\right)$
19 18 rspccv ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\to \left(\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)\in {A}\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)+1\in {A}\right)$
20 19 ad2antlr ${⊢}\left(\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\wedge {z}\in \mathrm{\omega }\right)\to \left(\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)\in {A}\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)+1\in {A}\right)$
21 ovex ${⊢}\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)+1\in \mathrm{V}$
22 eqid ${⊢}{\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}={\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}$
23 oveq1 ${⊢}{y}={n}\to {y}+1={n}+1$
24 oveq1 ${⊢}{y}=\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)\to {y}+1=\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)+1$
25 22 23 24 frsucmpt2 ${⊢}\left({z}\in \mathrm{\omega }\wedge \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)+1\in \mathrm{V}\right)\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{z}\right)=\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)+1$
26 21 25 mpan2 ${⊢}{z}\in \mathrm{\omega }\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{z}\right)=\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)+1$
27 26 eleq1d ${⊢}{z}\in \mathrm{\omega }\to \left(\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{z}\right)\in {A}↔\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)+1\in {A}\right)$
28 27 adantl ${⊢}\left(\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\wedge {z}\in \mathrm{\omega }\right)\to \left(\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{z}\right)\in {A}↔\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)+1\in {A}\right)$
29 20 28 sylibrd ${⊢}\left(\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\wedge {z}\in \mathrm{\omega }\right)\to \left(\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)\in {A}\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{z}\right)\in {A}\right)$
30 29 expcom ${⊢}{z}\in \mathrm{\omega }\to \left(\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\to \left(\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({z}\right)\in {A}\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{z}\right)\in {A}\right)\right)$
31 7 9 11 16 30 finds2 ${⊢}{y}\in \mathrm{\omega }\to \left(\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)\in {A}\right)$
32 31 com12 ${⊢}\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\to \left({y}\in \mathrm{\omega }\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)\in {A}\right)$
33 32 ralrimiv ${⊢}\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\to \forall {y}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)\in {A}$
34 ffnfv ${⊢}\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right):\mathrm{\omega }⟶{A}↔\left(\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)Fn\mathrm{\omega }\wedge \forall {y}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\left({y}\right)\in {A}\right)$
35 5 33 34 sylanbrc ${⊢}\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\to \left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right):\mathrm{\omega }⟶{A}$
36 35 frnd ${⊢}\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\to \mathrm{ran}\left({\mathrm{rec}\left(\left({n}\in \mathrm{V}⟼{n}+1\right),1\right)↾}_{\mathrm{\omega }}\right)\subseteq {A}$
37 3 36 eqsstrid ${⊢}\left(1\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}+1\in {A}\right)\to ℕ\subseteq {A}$