Metamath Proof Explorer

Theorem peano5

Description: The induction postulate: any class containing zero and closed under the successor operation contains all natural numbers. One of Peano's five postulates for arithmetic. Proposition 7.30(5) of TakeutiZaring p. 43, except our proof does not require the Axiom of Infinity. The more traditional statement of mathematical induction as a theorem schema, with a basis and an induction step, is derived from this theorem as theorem findes . (Contributed by NM, 18-Feb-2004)

Ref Expression
Assertion peano5 ${⊢}\left(\varnothing \in {A}\wedge \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\right)\to \mathrm{\omega }\subseteq {A}$

Proof

Step Hyp Ref Expression
1 eldifn ${⊢}{y}\in \left(\mathrm{\omega }\setminus {A}\right)\to ¬{y}\in {A}$
2 1 adantl ${⊢}\left(\left(\varnothing \in {A}\wedge \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\right)\wedge {y}\in \left(\mathrm{\omega }\setminus {A}\right)\right)\to ¬{y}\in {A}$
3 eldifi ${⊢}{y}\in \left(\mathrm{\omega }\setminus {A}\right)\to {y}\in \mathrm{\omega }$
4 elndif ${⊢}\varnothing \in {A}\to ¬\varnothing \in \left(\mathrm{\omega }\setminus {A}\right)$
5 eleq1 ${⊢}{y}=\varnothing \to \left({y}\in \left(\mathrm{\omega }\setminus {A}\right)↔\varnothing \in \left(\mathrm{\omega }\setminus {A}\right)\right)$
6 5 biimpcd ${⊢}{y}\in \left(\mathrm{\omega }\setminus {A}\right)\to \left({y}=\varnothing \to \varnothing \in \left(\mathrm{\omega }\setminus {A}\right)\right)$
7 6 necon3bd ${⊢}{y}\in \left(\mathrm{\omega }\setminus {A}\right)\to \left(¬\varnothing \in \left(\mathrm{\omega }\setminus {A}\right)\to {y}\ne \varnothing \right)$
8 4 7 mpan9 ${⊢}\left(\varnothing \in {A}\wedge {y}\in \left(\mathrm{\omega }\setminus {A}\right)\right)\to {y}\ne \varnothing$
9 nnsuc ${⊢}\left({y}\in \mathrm{\omega }\wedge {y}\ne \varnothing \right)\to \exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{y}=\mathrm{suc}{x}$
10 3 8 9 syl2an2 ${⊢}\left(\varnothing \in {A}\wedge {y}\in \left(\mathrm{\omega }\setminus {A}\right)\right)\to \exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{y}=\mathrm{suc}{x}$
11 10 ad4ant13 ${⊢}\left(\left(\left(\varnothing \in {A}\wedge \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\right)\wedge {y}\in \left(\mathrm{\omega }\setminus {A}\right)\right)\wedge \left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \right)\to \exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{y}=\mathrm{suc}{x}$
12 nfra1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)$
13 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}\in \left(\mathrm{\omega }\setminus {A}\right)\wedge \left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \right)$
14 12 13 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\wedge \left({y}\in \left(\mathrm{\omega }\setminus {A}\right)\wedge \left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \right)\right)$
15 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
16 rsp ${⊢}\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\to \left({x}\in \mathrm{\omega }\to \left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\right)$
17 vex ${⊢}{x}\in \mathrm{V}$
18 17 sucid ${⊢}{x}\in \mathrm{suc}{x}$
19 eleq2 ${⊢}{y}=\mathrm{suc}{x}\to \left({x}\in {y}↔{x}\in \mathrm{suc}{x}\right)$
20 18 19 mpbiri ${⊢}{y}=\mathrm{suc}{x}\to {x}\in {y}$
21 eleq1 ${⊢}{y}=\mathrm{suc}{x}\to \left({y}\in \mathrm{\omega }↔\mathrm{suc}{x}\in \mathrm{\omega }\right)$
22 peano2b ${⊢}{x}\in \mathrm{\omega }↔\mathrm{suc}{x}\in \mathrm{\omega }$
23 21 22 syl6bbr ${⊢}{y}=\mathrm{suc}{x}\to \left({y}\in \mathrm{\omega }↔{x}\in \mathrm{\omega }\right)$
24 minel ${⊢}\left({x}\in {y}\wedge \left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \right)\to ¬{x}\in \left(\mathrm{\omega }\setminus {A}\right)$
25 neldif ${⊢}\left({x}\in \mathrm{\omega }\wedge ¬{x}\in \left(\mathrm{\omega }\setminus {A}\right)\right)\to {x}\in {A}$
26 24 25 sylan2 ${⊢}\left({x}\in \mathrm{\omega }\wedge \left({x}\in {y}\wedge \left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \right)\right)\to {x}\in {A}$
27 26 exp32 ${⊢}{x}\in \mathrm{\omega }\to \left({x}\in {y}\to \left(\left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \to {x}\in {A}\right)\right)$
28 23 27 syl6bi ${⊢}{y}=\mathrm{suc}{x}\to \left({y}\in \mathrm{\omega }\to \left({x}\in {y}\to \left(\left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \to {x}\in {A}\right)\right)\right)$
29 20 28 mpid ${⊢}{y}=\mathrm{suc}{x}\to \left({y}\in \mathrm{\omega }\to \left(\left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \to {x}\in {A}\right)\right)$
30 3 29 syl5 ${⊢}{y}=\mathrm{suc}{x}\to \left({y}\in \left(\mathrm{\omega }\setminus {A}\right)\to \left(\left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \to {x}\in {A}\right)\right)$
31 30 impd ${⊢}{y}=\mathrm{suc}{x}\to \left(\left({y}\in \left(\mathrm{\omega }\setminus {A}\right)\wedge \left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \right)\to {x}\in {A}\right)$
32 eleq1a ${⊢}\mathrm{suc}{x}\in {A}\to \left({y}=\mathrm{suc}{x}\to {y}\in {A}\right)$
33 32 com12 ${⊢}{y}=\mathrm{suc}{x}\to \left(\mathrm{suc}{x}\in {A}\to {y}\in {A}\right)$
34 31 33 imim12d ${⊢}{y}=\mathrm{suc}{x}\to \left(\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\to \left(\left({y}\in \left(\mathrm{\omega }\setminus {A}\right)\wedge \left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \right)\to {y}\in {A}\right)\right)$
35 34 com13 ${⊢}\left({y}\in \left(\mathrm{\omega }\setminus {A}\right)\wedge \left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \right)\to \left(\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\to \left({y}=\mathrm{suc}{x}\to {y}\in {A}\right)\right)$
36 16 35 sylan9 ${⊢}\left(\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\wedge \left({y}\in \left(\mathrm{\omega }\setminus {A}\right)\wedge \left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \right)\right)\to \left({x}\in \mathrm{\omega }\to \left({y}=\mathrm{suc}{x}\to {y}\in {A}\right)\right)$
37 14 15 36 rexlimd ${⊢}\left(\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\wedge \left({y}\in \left(\mathrm{\omega }\setminus {A}\right)\wedge \left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \right)\right)\to \left(\exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{y}=\mathrm{suc}{x}\to {y}\in {A}\right)$
38 37 exp32 ${⊢}\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\to \left({y}\in \left(\mathrm{\omega }\setminus {A}\right)\to \left(\left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \to \left(\exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{y}=\mathrm{suc}{x}\to {y}\in {A}\right)\right)\right)$
39 38 a1i ${⊢}\varnothing \in {A}\to \left(\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\to \left({y}\in \left(\mathrm{\omega }\setminus {A}\right)\to \left(\left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \to \left(\exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{y}=\mathrm{suc}{x}\to {y}\in {A}\right)\right)\right)\right)$
40 39 imp41 ${⊢}\left(\left(\left(\varnothing \in {A}\wedge \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\right)\wedge {y}\in \left(\mathrm{\omega }\setminus {A}\right)\right)\wedge \left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \right)\to \left(\exists {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{y}=\mathrm{suc}{x}\to {y}\in {A}\right)$
41 11 40 mpd ${⊢}\left(\left(\left(\varnothing \in {A}\wedge \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\right)\wedge {y}\in \left(\mathrm{\omega }\setminus {A}\right)\right)\wedge \left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \right)\to {y}\in {A}$
42 2 41 mtand ${⊢}\left(\left(\varnothing \in {A}\wedge \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\right)\wedge {y}\in \left(\mathrm{\omega }\setminus {A}\right)\right)\to ¬\left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing$
43 42 nrexdv ${⊢}\left(\varnothing \in {A}\wedge \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\right)\to ¬\exists {y}\in \left(\mathrm{\omega }\setminus {A}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing$
44 ordom ${⊢}\mathrm{Ord}\mathrm{\omega }$
45 difss ${⊢}\mathrm{\omega }\setminus {A}\subseteq \mathrm{\omega }$
46 tz7.5 ${⊢}\left(\mathrm{Ord}\mathrm{\omega }\wedge \mathrm{\omega }\setminus {A}\subseteq \mathrm{\omega }\wedge \mathrm{\omega }\setminus {A}\ne \varnothing \right)\to \exists {y}\in \left(\mathrm{\omega }\setminus {A}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing$
47 44 45 46 mp3an12 ${⊢}\mathrm{\omega }\setminus {A}\ne \varnothing \to \exists {y}\in \left(\mathrm{\omega }\setminus {A}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing$
48 47 necon1bi ${⊢}¬\exists {y}\in \left(\mathrm{\omega }\setminus {A}\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{\omega }\setminus {A}\right)\cap {y}=\varnothing \to \mathrm{\omega }\setminus {A}=\varnothing$
49 43 48 syl ${⊢}\left(\varnothing \in {A}\wedge \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\right)\to \mathrm{\omega }\setminus {A}=\varnothing$
50 ssdif0 ${⊢}\mathrm{\omega }\subseteq {A}↔\mathrm{\omega }\setminus {A}=\varnothing$
51 49 50 sylibr ${⊢}\left(\varnothing \in {A}\wedge \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \mathrm{suc}{x}\in {A}\right)\right)\to \mathrm{\omega }\subseteq {A}$