MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  peano5 Structured version   Visualization version   GIF version

Theorem peano5 7888
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 7897. (Contributed by NM, 18-Feb-2004.) Avoid ax-10 2135, ax-12 2169. (Revised by Gino Giotto, 3-Oct-2024.)
Assertion
Ref Expression
peano5 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ω ⊆ 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem peano5
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldifn 4128 . . . . . 6 (𝑧 ∈ (ω ∖ 𝐴) → ¬ 𝑧𝐴)
21adantl 480 . . . . 5 (((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) → ¬ 𝑧𝐴)
3 eldifi 4127 . . . . . . . 8 (𝑧 ∈ (ω ∖ 𝐴) → 𝑧 ∈ ω)
4 elndif 4129 . . . . . . . . 9 (∅ ∈ 𝐴 → ¬ ∅ ∈ (ω ∖ 𝐴))
5 eleq1 2819 . . . . . . . . . . 11 (𝑧 = ∅ → (𝑧 ∈ (ω ∖ 𝐴) ↔ ∅ ∈ (ω ∖ 𝐴)))
65biimpcd 248 . . . . . . . . . 10 (𝑧 ∈ (ω ∖ 𝐴) → (𝑧 = ∅ → ∅ ∈ (ω ∖ 𝐴)))
76necon3bd 2952 . . . . . . . . 9 (𝑧 ∈ (ω ∖ 𝐴) → (¬ ∅ ∈ (ω ∖ 𝐴) → 𝑧 ≠ ∅))
84, 7mpan9 505 . . . . . . . 8 ((∅ ∈ 𝐴𝑧 ∈ (ω ∖ 𝐴)) → 𝑧 ≠ ∅)
9 nnsuc 7877 . . . . . . . 8 ((𝑧 ∈ ω ∧ 𝑧 ≠ ∅) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
103, 8, 9syl2an2 682 . . . . . . 7 ((∅ ∈ 𝐴𝑧 ∈ (ω ∖ 𝐴)) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
1110ad4ant13 747 . . . . . 6 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
12 eleq1w 2814 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
13 suceq 6431 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
1413eleq1d 2816 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (suc 𝑥𝐴 ↔ suc 𝑦𝐴))
1512, 14imbi12d 343 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑥𝐴 → suc 𝑥𝐴) ↔ (𝑦𝐴 → suc 𝑦𝐴)))
1615rspccv 3610 . . . . . . . . . . 11 (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑦 ∈ ω → (𝑦𝐴 → suc 𝑦𝐴)))
17 vex 3476 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
1817sucid 6447 . . . . . . . . . . . . . . . . 17 𝑦 ∈ suc 𝑦
19 eleq2 2820 . . . . . . . . . . . . . . . . 17 (𝑧 = suc 𝑦 → (𝑦𝑧𝑦 ∈ suc 𝑦))
2018, 19mpbiri 257 . . . . . . . . . . . . . . . 16 (𝑧 = suc 𝑦𝑦𝑧)
21 eleq1 2819 . . . . . . . . . . . . . . . . . 18 (𝑧 = suc 𝑦 → (𝑧 ∈ ω ↔ suc 𝑦 ∈ ω))
22 peano2b 7876 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
2321, 22bitr4di 288 . . . . . . . . . . . . . . . . 17 (𝑧 = suc 𝑦 → (𝑧 ∈ ω ↔ 𝑦 ∈ ω))
24 minel 4466 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑧 ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ¬ 𝑦 ∈ (ω ∖ 𝐴))
25 neldif 4130 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ω ∧ ¬ 𝑦 ∈ (ω ∖ 𝐴)) → 𝑦𝐴)
2624, 25sylan2 591 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ω ∧ (𝑦𝑧 ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)) → 𝑦𝐴)
2726exp32 419 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ω → (𝑦𝑧 → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴)))
2823, 27syl6bi 252 . . . . . . . . . . . . . . . 16 (𝑧 = suc 𝑦 → (𝑧 ∈ ω → (𝑦𝑧 → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴))))
2920, 28mpid 44 . . . . . . . . . . . . . . 15 (𝑧 = suc 𝑦 → (𝑧 ∈ ω → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴)))
303, 29syl5 34 . . . . . . . . . . . . . 14 (𝑧 = suc 𝑦 → (𝑧 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴)))
3130impd 409 . . . . . . . . . . . . 13 (𝑧 = suc 𝑦 → ((𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → 𝑦𝐴))
32 eleq1a 2826 . . . . . . . . . . . . . 14 (suc 𝑦𝐴 → (𝑧 = suc 𝑦𝑧𝐴))
3332com12 32 . . . . . . . . . . . . 13 (𝑧 = suc 𝑦 → (suc 𝑦𝐴𝑧𝐴))
3431, 33imim12d 81 . . . . . . . . . . . 12 (𝑧 = suc 𝑦 → ((𝑦𝐴 → suc 𝑦𝐴) → ((𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → 𝑧𝐴)))
3534com13 88 . . . . . . . . . . 11 ((𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ((𝑦𝐴 → suc 𝑦𝐴) → (𝑧 = suc 𝑦𝑧𝐴)))
3616, 35sylan9 506 . . . . . . . . . 10 ((∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) ∧ (𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)) → (𝑦 ∈ ω → (𝑧 = suc 𝑦𝑧𝐴)))
3736rexlimdv 3151 . . . . . . . . 9 ((∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) ∧ (𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)) → (∃𝑦 ∈ ω 𝑧 = suc 𝑦𝑧𝐴))
3837exp32 419 . . . . . . . 8 (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑧 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → (∃𝑦 ∈ ω 𝑧 = suc 𝑦𝑧𝐴))))
3938a1i 11 . . . . . . 7 (∅ ∈ 𝐴 → (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑧 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → (∃𝑦 ∈ ω 𝑧 = suc 𝑦𝑧𝐴)))))
4039imp41 424 . . . . . 6 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → (∃𝑦 ∈ ω 𝑧 = suc 𝑦𝑧𝐴))
4111, 40mpd 15 . . . . 5 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → 𝑧𝐴)
422, 41mtand 812 . . . 4 (((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) → ¬ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4342nrexdv 3147 . . 3 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ¬ ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
44 ordom 7869 . . . . 5 Ord ω
45 difss 4132 . . . . 5 (ω ∖ 𝐴) ⊆ ω
46 tz7.5 6386 . . . . 5 ((Ord ω ∧ (ω ∖ 𝐴) ⊆ ω ∧ (ω ∖ 𝐴) ≠ ∅) → ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4744, 45, 46mp3an12 1449 . . . 4 ((ω ∖ 𝐴) ≠ ∅ → ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4847necon1bi 2967 . . 3 (¬ ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅ → (ω ∖ 𝐴) = ∅)
4943, 48syl 17 . 2 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → (ω ∖ 𝐴) = ∅)
50 ssdif0 4364 . 2 (ω ⊆ 𝐴 ↔ (ω ∖ 𝐴) = ∅)
5149, 50sylibr 233 1 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ω ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394   = wceq 1539  wcel 2104  wne 2938  wral 3059  wrex 3068  cdif 3946  cin 3948  wss 3949  c0 4323  Ord word 6364  suc csuc 6367  ωcom 7859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-om 7860
This theorem is referenced by:  find  7891  findOLD  7892  finds  7893  finds2  7895  omex  9642  dfom3  9646
  Copyright terms: Public domain W3C validator