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) Avoid ax-10 , ax-12 . (Revised by GG, 3-Oct-2024)

Ref Expression
Assertion peano5 ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ω ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 eldifn ⊢ ( 𝑧 ∈ ( ω ∖ 𝐴 ) → ¬ 𝑧 ∈ 𝐴 )
2 1 adantl ⊢ ( ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ω ∖ 𝐴 ) ) → ¬ 𝑧 ∈ 𝐴 )
3 eldifi ⊢ ( 𝑧 ∈ ( ω ∖ 𝐴 ) → 𝑧 ∈ ω )
4 elndif ⊢ ( ∅ ∈ 𝐴 → ¬ ∅ ∈ ( ω ∖ 𝐴 ) )
5 eleq1 ⊢ ( 𝑧 = ∅ → ( 𝑧 ∈ ( ω ∖ 𝐴 ) ↔ ∅ ∈ ( ω ∖ 𝐴 ) ) )
6 5 biimpcd ⊢ ( 𝑧 ∈ ( ω ∖ 𝐴 ) → ( 𝑧 = ∅ → ∅ ∈ ( ω ∖ 𝐴 ) ) )
7 6 necon3bd ⊢ ( 𝑧 ∈ ( ω ∖ 𝐴 ) → ( ¬ ∅ ∈ ( ω ∖ 𝐴 ) → 𝑧 ≠ ∅ ) )
8 4 7 mpan9 ⊢ ( ( ∅ ∈ 𝐴 ∧ 𝑧 ∈ ( ω ∖ 𝐴 ) ) → 𝑧 ≠ ∅ )
9 nnsuc ⊢ ( ( 𝑧 ∈ ω ∧ 𝑧 ≠ ∅ ) → ∃ 𝑦 ∈ ω 𝑧 = suc 𝑦 )
10 3 8 9 syl2an2 ⊢ ( ( ∅ ∈ 𝐴 ∧ 𝑧 ∈ ( ω ∖ 𝐴 ) ) → ∃ 𝑦 ∈ ω 𝑧 = suc 𝑦 )
11 10 ad4ant13 ⊢ ( ( ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ω ∖ 𝐴 ) ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ ) → ∃ 𝑦 ∈ ω 𝑧 = suc 𝑦 )
12 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
13 suceq ⊢ ( 𝑥 = 𝑦 → suc 𝑥 = suc 𝑦 )
14 13 eleq1d ⊢ ( 𝑥 = 𝑦 → ( suc 𝑥 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴 ) )
15 12 14 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝐴 → suc 𝑦 ∈ 𝐴 ) ) )
16 15 rspccv ⊢ ( ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ω → ( 𝑦 ∈ 𝐴 → suc 𝑦 ∈ 𝐴 ) ) )
17 vex ⊢ 𝑦 ∈ V
18 17 sucid ⊢ 𝑦 ∈ suc 𝑦
19 eleq2 ⊢ ( 𝑧 = suc 𝑦 → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ suc 𝑦 ) )
20 18 19 mpbiri ⊢ ( 𝑧 = suc 𝑦 → 𝑦 ∈ 𝑧 )
21 eleq1 ⊢ ( 𝑧 = suc 𝑦 → ( 𝑧 ∈ ω ↔ suc 𝑦 ∈ ω ) )
22 peano2b ⊢ ( 𝑦 ∈ ω ↔ suc 𝑦 ∈ ω )
23 21 22 bitr4di ⊢ ( 𝑧 = suc 𝑦 → ( 𝑧 ∈ ω ↔ 𝑦 ∈ ω ) )
24 minel ⊢ ( ( 𝑦 ∈ 𝑧 ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ ) → ¬ 𝑦 ∈ ( ω ∖ 𝐴 ) )
25 neldif ⊢ ( ( 𝑦 ∈ ω ∧ ¬ 𝑦 ∈ ( ω ∖ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
26 24 25 sylan2 ⊢ ( ( 𝑦 ∈ ω ∧ ( 𝑦 ∈ 𝑧 ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ ) ) → 𝑦 ∈ 𝐴 )
27 26 exp32 ⊢ ( 𝑦 ∈ ω → ( 𝑦 ∈ 𝑧 → ( ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ → 𝑦 ∈ 𝐴 ) ) )
28 23 27 biimtrdi ⊢ ( 𝑧 = suc 𝑦 → ( 𝑧 ∈ ω → ( 𝑦 ∈ 𝑧 → ( ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ → 𝑦 ∈ 𝐴 ) ) ) )
29 20 28 mpid ⊢ ( 𝑧 = suc 𝑦 → ( 𝑧 ∈ ω → ( ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ → 𝑦 ∈ 𝐴 ) ) )
30 3 29 syl5 ⊢ ( 𝑧 = suc 𝑦 → ( 𝑧 ∈ ( ω ∖ 𝐴 ) → ( ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ → 𝑦 ∈ 𝐴 ) ) )
31 30 impd ⊢ ( 𝑧 = suc 𝑦 → ( ( 𝑧 ∈ ( ω ∖ 𝐴 ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ ) → 𝑦 ∈ 𝐴 ) )
32 eleq1a ⊢ ( suc 𝑦 ∈ 𝐴 → ( 𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴 ) )
33 32 com12 ⊢ ( 𝑧 = suc 𝑦 → ( suc 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) )
34 31 33 imim12d ⊢ ( 𝑧 = suc 𝑦 → ( ( 𝑦 ∈ 𝐴 → suc 𝑦 ∈ 𝐴 ) → ( ( 𝑧 ∈ ( ω ∖ 𝐴 ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ ) → 𝑧 ∈ 𝐴 ) ) )
35 34 com13 ⊢ ( ( 𝑧 ∈ ( ω ∖ 𝐴 ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ ) → ( ( 𝑦 ∈ 𝐴 → suc 𝑦 ∈ 𝐴 ) → ( 𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴 ) ) )
36 16 35 sylan9 ⊢ ( ( ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( ω ∖ 𝐴 ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ ) ) → ( 𝑦 ∈ ω → ( 𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴 ) ) )
37 36 rexlimdv ⊢ ( ( ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( ω ∖ 𝐴 ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ ) ) → ( ∃ 𝑦 ∈ ω 𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴 ) )
38 37 exp32 ⊢ ( ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) → ( 𝑧 ∈ ( ω ∖ 𝐴 ) → ( ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ → ( ∃ 𝑦 ∈ ω 𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴 ) ) ) )
39 38 a1i ⊢ ( ∅ ∈ 𝐴 → ( ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) → ( 𝑧 ∈ ( ω ∖ 𝐴 ) → ( ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ → ( ∃ 𝑦 ∈ ω 𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴 ) ) ) ) )
40 39 imp41 ⊢ ( ( ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ω ∖ 𝐴 ) ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ ) → ( ∃ 𝑦 ∈ ω 𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴 ) )
41 11 40 mpd ⊢ ( ( ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ω ∖ 𝐴 ) ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ ) → 𝑧 ∈ 𝐴 )
42 2 41 mtand ⊢ ( ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ω ∖ 𝐴 ) ) → ¬ ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ )
43 42 nrexdv ⊢ ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ¬ ∃ 𝑧 ∈ ( ω ∖ 𝐴 ) ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ )
44 ordom ⊢ Ord ω
45 difss ⊢ ( ω ∖ 𝐴 ) ⊆ ω
46 tz7.5 ⊢ ( ( Ord ω ∧ ( ω ∖ 𝐴 ) ⊆ ω ∧ ( ω ∖ 𝐴 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( ω ∖ 𝐴 ) ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ )
47 44 45 46 mp3an12 ⊢ ( ( ω ∖ 𝐴 ) ≠ ∅ → ∃ 𝑧 ∈ ( ω ∖ 𝐴 ) ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ )
48 47 necon1bi ⊢ ( ¬ ∃ 𝑧 ∈ ( ω ∖ 𝐴 ) ( ( ω ∖ 𝐴 ) ∩ 𝑧 ) = ∅ → ( ω ∖ 𝐴 ) = ∅ )
49 43 48 syl ⊢ ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ( ω ∖ 𝐴 ) = ∅ )
50 ssdif0 ⊢ ( ω ⊆ 𝐴 ↔ ( ω ∖ 𝐴 ) = ∅ )
51 49 50 sylibr ⊢ ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ω ⊆ 𝐴 )