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

Theorem peano5 7916
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 7923. (Contributed by NM, 18-Feb-2004.) Avoid ax-10 2139, ax-12 2175. (Revised by GG, 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 4142 . . . . . 6 (𝑧 ∈ (ω ∖ 𝐴) → ¬ 𝑧𝐴)
21adantl 481 . . . . 5 (((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) → ¬ 𝑧𝐴)
3 eldifi 4141 . . . . . . . 8 (𝑧 ∈ (ω ∖ 𝐴) → 𝑧 ∈ ω)
4 elndif 4143 . . . . . . . . 9 (∅ ∈ 𝐴 → ¬ ∅ ∈ (ω ∖ 𝐴))
5 eleq1 2827 . . . . . . . . . . 11 (𝑧 = ∅ → (𝑧 ∈ (ω ∖ 𝐴) ↔ ∅ ∈ (ω ∖ 𝐴)))
65biimpcd 249 . . . . . . . . . 10 (𝑧 ∈ (ω ∖ 𝐴) → (𝑧 = ∅ → ∅ ∈ (ω ∖ 𝐴)))
76necon3bd 2952 . . . . . . . . 9 (𝑧 ∈ (ω ∖ 𝐴) → (¬ ∅ ∈ (ω ∖ 𝐴) → 𝑧 ≠ ∅))
84, 7mpan9 506 . . . . . . . 8 ((∅ ∈ 𝐴𝑧 ∈ (ω ∖ 𝐴)) → 𝑧 ≠ ∅)
9 nnsuc 7905 . . . . . . . 8 ((𝑧 ∈ ω ∧ 𝑧 ≠ ∅) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
103, 8, 9syl2an2 686 . . . . . . 7 ((∅ ∈ 𝐴𝑧 ∈ (ω ∖ 𝐴)) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
1110ad4ant13 751 . . . . . 6 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
12 eleq1w 2822 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
13 suceq 6452 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
1413eleq1d 2824 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (suc 𝑥𝐴 ↔ suc 𝑦𝐴))
1512, 14imbi12d 344 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑥𝐴 → suc 𝑥𝐴) ↔ (𝑦𝐴 → suc 𝑦𝐴)))
1615rspccv 3619 . . . . . . . . . . 11 (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑦 ∈ ω → (𝑦𝐴 → suc 𝑦𝐴)))
17 vex 3482 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
1817sucid 6468 . . . . . . . . . . . . . . . . 17 𝑦 ∈ suc 𝑦
19 eleq2 2828 . . . . . . . . . . . . . . . . 17 (𝑧 = suc 𝑦 → (𝑦𝑧𝑦 ∈ suc 𝑦))
2018, 19mpbiri 258 . . . . . . . . . . . . . . . 16 (𝑧 = suc 𝑦𝑦𝑧)
21 eleq1 2827 . . . . . . . . . . . . . . . . . 18 (𝑧 = suc 𝑦 → (𝑧 ∈ ω ↔ suc 𝑦 ∈ ω))
22 peano2b 7904 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
2321, 22bitr4di 289 . . . . . . . . . . . . . . . . 17 (𝑧 = suc 𝑦 → (𝑧 ∈ ω ↔ 𝑦 ∈ ω))
24 minel 4472 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑧 ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ¬ 𝑦 ∈ (ω ∖ 𝐴))
25 neldif 4144 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ω ∧ ¬ 𝑦 ∈ (ω ∖ 𝐴)) → 𝑦𝐴)
2624, 25sylan2 593 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ω ∧ (𝑦𝑧 ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)) → 𝑦𝐴)
2726exp32 420 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ω → (𝑦𝑧 → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴)))
2823, 27biimtrdi 253 . . . . . . . . . . . . . . . 16 (𝑧 = suc 𝑦 → (𝑧 ∈ ω → (𝑦𝑧 → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴))))
2920, 28mpid 44 . . . . . . . . . . . . . . 15 (𝑧 = suc 𝑦 → (𝑧 ∈ ω → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴)))
303, 29syl5 34 . . . . . . . . . . . . . 14 (𝑧 = suc 𝑦 → (𝑧 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴)))
3130impd 410 . . . . . . . . . . . . 13 (𝑧 = suc 𝑦 → ((𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → 𝑦𝐴))
32 eleq1a 2834 . . . . . . . . . . . . . 14 (suc 𝑦𝐴 → (𝑧 = suc 𝑦𝑧𝐴))
3332com12 32 . . . . . . . . . . . . 13 (𝑧 = suc 𝑦 → (suc 𝑦𝐴𝑧𝐴))
3431, 33imim12d 81 . . . . . . . . . . . 12 (𝑧 = suc 𝑦 → ((𝑦𝐴 → suc 𝑦𝐴) → ((𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → 𝑧𝐴)))
3534com13 88 . . . . . . . . . . 11 ((𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ((𝑦𝐴 → suc 𝑦𝐴) → (𝑧 = suc 𝑦𝑧𝐴)))
3616, 35sylan9 507 . . . . . . . . . 10 ((∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) ∧ (𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)) → (𝑦 ∈ ω → (𝑧 = suc 𝑦𝑧𝐴)))
3736rexlimdv 3151 . . . . . . . . 9 ((∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) ∧ (𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)) → (∃𝑦 ∈ ω 𝑧 = suc 𝑦𝑧𝐴))
3837exp32 420 . . . . . . . 8 (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑧 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → (∃𝑦 ∈ ω 𝑧 = suc 𝑦𝑧𝐴))))
3938a1i 11 . . . . . . 7 (∅ ∈ 𝐴 → (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑧 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → (∃𝑦 ∈ ω 𝑧 = suc 𝑦𝑧𝐴)))))
4039imp41 425 . . . . . 6 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → (∃𝑦 ∈ ω 𝑧 = suc 𝑦𝑧𝐴))
4111, 40mpd 15 . . . . 5 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → 𝑧𝐴)
422, 41mtand 816 . . . 4 (((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) → ¬ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4342nrexdv 3147 . . 3 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ¬ ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
44 ordom 7897 . . . . 5 Ord ω
45 difss 4146 . . . . 5 (ω ∖ 𝐴) ⊆ ω
46 tz7.5 6407 . . . . 5 ((Ord ω ∧ (ω ∖ 𝐴) ⊆ ω ∧ (ω ∖ 𝐴) ≠ ∅) → ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4744, 45, 46mp3an12 1450 . . . 4 ((ω ∖ 𝐴) ≠ ∅ → ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4847necon1bi 2967 . . 3 (¬ ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅ → (ω ∖ 𝐴) = ∅)
4943, 48syl 17 . 2 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → (ω ∖ 𝐴) = ∅)
50 ssdif0 4372 . 2 (ω ⊆ 𝐴 ↔ (ω ∖ 𝐴) = ∅)
5149, 50sylibr 234 1 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ω ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1537  wcel 2106  wne 2938  wral 3059  wrex 3068  cdif 3960  cin 3962  wss 3963  c0 4339  Ord word 6385  suc csuc 6388  ωcom 7887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-om 7888
This theorem is referenced by:  find  7918  finds  7919  finds2  7921  omex  9681  dfom3  9685
  Copyright terms: Public domain W3C validator