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

Theorem peano5 7905
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 7914. (Contributed by NM, 18-Feb-2004.) Avoid ax-10 2129, ax-12 2166. (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 2817 . . . . . . . . . . 11 (𝑧 = ∅ → (𝑧 ∈ (ω ∖ 𝐴) ↔ ∅ ∈ (ω ∖ 𝐴)))
65biimpcd 248 . . . . . . . . . 10 (𝑧 ∈ (ω ∖ 𝐴) → (𝑧 = ∅ → ∅ ∈ (ω ∖ 𝐴)))
76necon3bd 2951 . . . . . . . . 9 (𝑧 ∈ (ω ∖ 𝐴) → (¬ ∅ ∈ (ω ∖ 𝐴) → 𝑧 ≠ ∅))
84, 7mpan9 505 . . . . . . . 8 ((∅ ∈ 𝐴𝑧 ∈ (ω ∖ 𝐴)) → 𝑧 ≠ ∅)
9 nnsuc 7894 . . . . . . . 8 ((𝑧 ∈ ω ∧ 𝑧 ≠ ∅) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
103, 8, 9syl2an2 684 . . . . . . 7 ((∅ ∈ 𝐴𝑧 ∈ (ω ∖ 𝐴)) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
1110ad4ant13 749 . . . . . 6 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
12 eleq1w 2812 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
13 suceq 6440 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
1413eleq1d 2814 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (suc 𝑥𝐴 ↔ suc 𝑦𝐴))
1512, 14imbi12d 343 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑥𝐴 → suc 𝑥𝐴) ↔ (𝑦𝐴 → suc 𝑦𝐴)))
1615rspccv 3608 . . . . . . . . . . 11 (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑦 ∈ ω → (𝑦𝐴 → suc 𝑦𝐴)))
17 vex 3477 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
1817sucid 6456 . . . . . . . . . . . . . . . . 17 𝑦 ∈ suc 𝑦
19 eleq2 2818 . . . . . . . . . . . . . . . . 17 (𝑧 = suc 𝑦 → (𝑦𝑧𝑦 ∈ suc 𝑦))
2018, 19mpbiri 257 . . . . . . . . . . . . . . . 16 (𝑧 = suc 𝑦𝑦𝑧)
21 eleq1 2817 . . . . . . . . . . . . . . . . . 18 (𝑧 = suc 𝑦 → (𝑧 ∈ ω ↔ suc 𝑦 ∈ ω))
22 peano2b 7893 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
2321, 22bitr4di 288 . . . . . . . . . . . . . . . . 17 (𝑧 = suc 𝑦 → (𝑧 ∈ ω ↔ 𝑦 ∈ ω))
24 minel 4469 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑧 ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ¬ 𝑦 ∈ (ω ∖ 𝐴))
25 neldif 4130 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ω ∧ ¬ 𝑦 ∈ (ω ∖ 𝐴)) → 𝑦𝐴)
2624, 25sylan2 591 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ω ∧ (𝑦𝑧 ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)) → 𝑦𝐴)
2726exp32 419 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ω → (𝑦𝑧 → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴)))
2823, 27biimtrdi 252 . . . . . . . . . . . . . . . 16 (𝑧 = suc 𝑦 → (𝑧 ∈ ω → (𝑦𝑧 → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴))))
2920, 28mpid 44 . . . . . . . . . . . . . . 15 (𝑧 = suc 𝑦 → (𝑧 ∈ ω → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴)))
303, 29syl5 34 . . . . . . . . . . . . . 14 (𝑧 = suc 𝑦 → (𝑧 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦𝐴)))
3130impd 409 . . . . . . . . . . . . 13 (𝑧 = suc 𝑦 → ((𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → 𝑦𝐴))
32 eleq1a 2824 . . . . . . . . . . . . . 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 3150 . . . . . . . . 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 814 . . . 4 (((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) → ¬ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4342nrexdv 3146 . . 3 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ¬ ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
44 ordom 7886 . . . . 5 Ord ω
45 difss 4132 . . . . 5 (ω ∖ 𝐴) ⊆ ω
46 tz7.5 6395 . . . . 5 ((Ord ω ∧ (ω ∖ 𝐴) ⊆ ω ∧ (ω ∖ 𝐴) ≠ ∅) → ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4744, 45, 46mp3an12 1447 . . . 4 ((ω ∖ 𝐴) ≠ ∅ → ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4847necon1bi 2966 . . 3 (¬ ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅ → (ω ∖ 𝐴) = ∅)
4943, 48syl 17 . 2 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → (ω ∖ 𝐴) = ∅)
50 ssdif0 4367 . 2 (ω ⊆ 𝐴 ↔ (ω ∖ 𝐴) = ∅)
5149, 50sylibr 233 1 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ω ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394   = wceq 1533  wcel 2098  wne 2937  wral 3058  wrex 3067  cdif 3946  cin 3948  wss 3949  c0 4326  Ord word 6373  suc csuc 6376  ωcom 7876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-tr 5270  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-om 7877
This theorem is referenced by:  find  7908  findOLD  7909  finds  7910  finds2  7912  omex  9674  dfom3  9678
  Copyright terms: Public domain W3C validator