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

Theorem peano5 7884
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 7893. (Contributed by NM, 18-Feb-2004.) Avoid ax-10 2138, ax-12 2172. (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 483 . . . . 5 (((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) → ¬ 𝑧𝐴)
3 eldifi 4127 . . . . . . . 8 (𝑧 ∈ (ω ∖ 𝐴) → 𝑧 ∈ ω)
4 elndif 4129 . . . . . . . . 9 (∅ ∈ 𝐴 → ¬ ∅ ∈ (ω ∖ 𝐴))
5 eleq1 2822 . . . . . . . . . . 11 (𝑧 = ∅ → (𝑧 ∈ (ω ∖ 𝐴) ↔ ∅ ∈ (ω ∖ 𝐴)))
65biimpcd 248 . . . . . . . . . 10 (𝑧 ∈ (ω ∖ 𝐴) → (𝑧 = ∅ → ∅ ∈ (ω ∖ 𝐴)))
76necon3bd 2955 . . . . . . . . 9 (𝑧 ∈ (ω ∖ 𝐴) → (¬ ∅ ∈ (ω ∖ 𝐴) → 𝑧 ≠ ∅))
84, 7mpan9 508 . . . . . . . 8 ((∅ ∈ 𝐴𝑧 ∈ (ω ∖ 𝐴)) → 𝑧 ≠ ∅)
9 nnsuc 7873 . . . . . . . 8 ((𝑧 ∈ ω ∧ 𝑧 ≠ ∅) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
103, 8, 9syl2an2 685 . . . . . . 7 ((∅ ∈ 𝐴𝑧 ∈ (ω ∖ 𝐴)) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
1110ad4ant13 750 . . . . . 6 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
12 eleq1w 2817 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
13 suceq 6431 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
1413eleq1d 2819 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (suc 𝑥𝐴 ↔ suc 𝑦𝐴))
1512, 14imbi12d 345 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑥𝐴 → suc 𝑥𝐴) ↔ (𝑦𝐴 → suc 𝑦𝐴)))
1615rspccv 3610 . . . . . . . . . . 11 (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑦 ∈ ω → (𝑦𝐴 → suc 𝑦𝐴)))
17 vex 3479 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
1817sucid 6447 . . . . . . . . . . . . . . . . 17 𝑦 ∈ suc 𝑦
19 eleq2 2823 . . . . . . . . . . . . . . . . 17 (𝑧 = suc 𝑦 → (𝑦𝑧𝑦 ∈ suc 𝑦))
2018, 19mpbiri 258 . . . . . . . . . . . . . . . 16 (𝑧 = suc 𝑦𝑦𝑧)
21 eleq1 2822 . . . . . . . . . . . . . . . . . 18 (𝑧 = suc 𝑦 → (𝑧 ∈ ω ↔ suc 𝑦 ∈ ω))
22 peano2b 7872 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
2321, 22bitr4di 289 . . . . . . . . . . . . . . . . 17 (𝑧 = suc 𝑦 → (𝑧 ∈ ω ↔ 𝑦 ∈ ω))
24 minel 4466 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑧 ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ¬ 𝑦 ∈ (ω ∖ 𝐴))
25 neldif 4130 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ω ∧ ¬ 𝑦 ∈ (ω ∖ 𝐴)) → 𝑦𝐴)
2624, 25sylan2 594 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ω ∧ (𝑦𝑧 ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)) → 𝑦𝐴)
2726exp32 422 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ω → (𝑦𝑧 → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴)))
2823, 27syl6bi 253 . . . . . . . . . . . . . . . 16 (𝑧 = suc 𝑦 → (𝑧 ∈ ω → (𝑦𝑧 → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴))))
2920, 28mpid 44 . . . . . . . . . . . . . . 15 (𝑧 = suc 𝑦 → (𝑧 ∈ ω → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴)))
303, 29syl5 34 . . . . . . . . . . . . . 14 (𝑧 = suc 𝑦 → (𝑧 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴)))
3130impd 412 . . . . . . . . . . . . 13 (𝑧 = suc 𝑦 → ((𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → 𝑦𝐴))
32 eleq1a 2829 . . . . . . . . . . . . . 14 (suc 𝑦𝐴 → (𝑧 = suc 𝑦𝑧𝐴))
3332com12 32 . . . . . . . . . . . . 13 (𝑧 = suc 𝑦 → (suc 𝑦𝐴𝑧𝐴))
3431, 33imim12d 81 . . . . . . . . . . . 12 (𝑧 = suc 𝑦 → ((𝑦𝐴 → suc 𝑦𝐴) → ((𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → 𝑧𝐴)))
3534com13 88 . . . . . . . . . . 11 ((𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ((𝑦𝐴 → suc 𝑦𝐴) → (𝑧 = suc 𝑦𝑧𝐴)))
3616, 35sylan9 509 . . . . . . . . . 10 ((∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) ∧ (𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)) → (𝑦 ∈ ω → (𝑧 = suc 𝑦𝑧𝐴)))
3736rexlimdv 3154 . . . . . . . . 9 ((∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) ∧ (𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)) → (∃𝑦 ∈ ω 𝑧 = suc 𝑦𝑧𝐴))
3837exp32 422 . . . . . . . 8 (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑧 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → (∃𝑦 ∈ ω 𝑧 = suc 𝑦𝑧𝐴))))
3938a1i 11 . . . . . . 7 (∅ ∈ 𝐴 → (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑧 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → (∃𝑦 ∈ ω 𝑧 = suc 𝑦𝑧𝐴)))))
4039imp41 427 . . . . . 6 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → (∃𝑦 ∈ ω 𝑧 = suc 𝑦𝑧𝐴))
4111, 40mpd 15 . . . . 5 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → 𝑧𝐴)
422, 41mtand 815 . . . 4 (((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) → ¬ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4342nrexdv 3150 . . 3 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ¬ ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
44 ordom 7865 . . . . 5 Ord ω
45 difss 4132 . . . . 5 (ω ∖ 𝐴) ⊆ ω
46 tz7.5 6386 . . . . 5 ((Ord ω ∧ (ω ∖ 𝐴) ⊆ ω ∧ (ω ∖ 𝐴) ≠ ∅) → ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4744, 45, 46mp3an12 1452 . . . 4 ((ω ∖ 𝐴) ≠ ∅ → ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4847necon1bi 2970 . . 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 397   = wceq 1542  wcel 2107  wne 2941  wral 3062  wrex 3071  cdif 3946  cin 3948  wss 3949  c0 4323  Ord word 6364  suc csuc 6367  ωcom 7855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  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 7856
This theorem is referenced by:  find  7887  findOLD  7888  finds  7889  finds2  7891  omex  9638  dfom3  9642
  Copyright terms: Public domain W3C validator