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

Theorem peano5 6793
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 6800. (Contributed by NM, 18-Feb-2004.)
Assertion
Ref Expression
peano5 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ω ⊆ 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem peano5
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eldifn 3581 . . . . . 6 (𝑦 ∈ (ω ∖ 𝐴) → ¬ 𝑦𝐴)
21adantl 475 . . . . 5 (((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) → ¬ 𝑦𝐴)
3 eldifi 3580 . . . . . . . . . 10 (𝑦 ∈ (ω ∖ 𝐴) → 𝑦 ∈ ω)
43adantl 475 . . . . . . . . 9 ((∅ ∈ 𝐴𝑦 ∈ (ω ∖ 𝐴)) → 𝑦 ∈ ω)
5 elndif 3582 . . . . . . . . . 10 (∅ ∈ 𝐴 → ¬ ∅ ∈ (ω ∖ 𝐴))
6 eleq1 2571 . . . . . . . . . . . 12 (𝑦 = ∅ → (𝑦 ∈ (ω ∖ 𝐴) ↔ ∅ ∈ (ω ∖ 𝐴)))
76biimpcd 234 . . . . . . . . . . 11 (𝑦 ∈ (ω ∖ 𝐴) → (𝑦 = ∅ → ∅ ∈ (ω ∖ 𝐴)))
87necon3bd 2691 . . . . . . . . . 10 (𝑦 ∈ (ω ∖ 𝐴) → (¬ ∅ ∈ (ω ∖ 𝐴) → 𝑦 ≠ ∅))
95, 8mpan9 479 . . . . . . . . 9 ((∅ ∈ 𝐴𝑦 ∈ (ω ∖ 𝐴)) → 𝑦 ≠ ∅)
10 nnsuc 6786 . . . . . . . . 9 ((𝑦 ∈ ω ∧ 𝑦 ≠ ∅) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥)
114, 9, 10syl2anc 682 . . . . . . . 8 ((∅ ∈ 𝐴𝑦 ∈ (ω ∖ 𝐴)) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥)
1211adantlr 738 . . . . . . 7 (((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥)
1312adantr 474 . . . . . 6 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥)
14 nfra1 2820 . . . . . . . . . . 11 𝑥𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)
15 nfv 1792 . . . . . . . . . . 11 𝑥(𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)
1614, 15nfan 2064 . . . . . . . . . 10 𝑥(∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) ∧ (𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅))
17 nfv 1792 . . . . . . . . . 10 𝑥 𝑦𝐴
18 rsp 2808 . . . . . . . . . . 11 (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑥 ∈ ω → (𝑥𝐴 → suc 𝑥𝐴)))
19 vex 3069 . . . . . . . . . . . . . . . . . 18 𝑥 ∈ V
2019sucid 5553 . . . . . . . . . . . . . . . . 17 𝑥 ∈ suc 𝑥
21 eleq2 2572 . . . . . . . . . . . . . . . . 17 (𝑦 = suc 𝑥 → (𝑥𝑦𝑥 ∈ suc 𝑥))
2220, 21mpbiri 243 . . . . . . . . . . . . . . . 16 (𝑦 = suc 𝑥𝑥𝑦)
23 eleq1 2571 . . . . . . . . . . . . . . . . . 18 (𝑦 = suc 𝑥 → (𝑦 ∈ ω ↔ suc 𝑥 ∈ ω))
24 peano2b 6785 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ω ↔ suc 𝑥 ∈ ω)
2523, 24syl6bbr 273 . . . . . . . . . . . . . . . . 17 (𝑦 = suc 𝑥 → (𝑦 ∈ ω ↔ 𝑥 ∈ ω))
26 minel 3860 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑦 ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → ¬ 𝑥 ∈ (ω ∖ 𝐴))
27 neldif 3583 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ω ∧ ¬ 𝑥 ∈ (ω ∖ 𝐴)) → 𝑥𝐴)
2826, 27sylan2 484 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ω ∧ (𝑥𝑦 ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)) → 𝑥𝐴)
2928exp32 622 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ω → (𝑥𝑦 → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → 𝑥𝐴)))
3025, 29syl6bi 238 . . . . . . . . . . . . . . . 16 (𝑦 = suc 𝑥 → (𝑦 ∈ ω → (𝑥𝑦 → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → 𝑥𝐴))))
3122, 30mpid 42 . . . . . . . . . . . . . . 15 (𝑦 = suc 𝑥 → (𝑦 ∈ ω → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → 𝑥𝐴)))
323, 31syl5 33 . . . . . . . . . . . . . 14 (𝑦 = suc 𝑥 → (𝑦 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → 𝑥𝐴)))
3332impd 440 . . . . . . . . . . . . 13 (𝑦 = suc 𝑥 → ((𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → 𝑥𝐴))
34 eleq1a 2578 . . . . . . . . . . . . . 14 (suc 𝑥𝐴 → (𝑦 = suc 𝑥𝑦𝐴))
3534com12 32 . . . . . . . . . . . . 13 (𝑦 = suc 𝑥 → (suc 𝑥𝐴𝑦𝐴))
3633, 35imim12d 78 . . . . . . . . . . . 12 (𝑦 = suc 𝑥 → ((𝑥𝐴 → suc 𝑥𝐴) → ((𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → 𝑦𝐴)))
3736com13 84 . . . . . . . . . . 11 ((𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → ((𝑥𝐴 → suc 𝑥𝐴) → (𝑦 = suc 𝑥𝑦𝐴)))
3818, 37sylan9 678 . . . . . . . . . 10 ((∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) ∧ (𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)) → (𝑥 ∈ ω → (𝑦 = suc 𝑥𝑦𝐴)))
3916, 17, 38rexlimd 2901 . . . . . . . . 9 ((∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) ∧ (𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)) → (∃𝑥 ∈ ω 𝑦 = suc 𝑥𝑦𝐴))
4039exp32 622 . . . . . . . 8 (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑦 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → (∃𝑥 ∈ ω 𝑦 = suc 𝑥𝑦𝐴))))
4140a1i 11 . . . . . . 7 (∅ ∈ 𝐴 → (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑦 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → (∃𝑥 ∈ ω 𝑦 = suc 𝑥𝑦𝐴)))))
4241imp41 610 . . . . . 6 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → (∃𝑥 ∈ ω 𝑦 = suc 𝑥𝑦𝐴))
4313, 42mpd 15 . . . . 5 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → 𝑦𝐴)
442, 43mtand 680 . . . 4 (((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) → ¬ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)
4544nrexdv 2877 . . 3 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ¬ ∃𝑦 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑦) = ∅)
46 ordom 6778 . . . . 5 Ord ω
47 difss 3585 . . . . 5 (ω ∖ 𝐴) ⊆ ω
48 tz7.5 5495 . . . . 5 ((Ord ω ∧ (ω ∖ 𝐴) ⊆ ω ∧ (ω ∖ 𝐴) ≠ ∅) → ∃𝑦 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑦) = ∅)
4946, 47, 48mp3an12 1396 . . . 4 ((ω ∖ 𝐴) ≠ ∅ → ∃𝑦 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑦) = ∅)
5049necon1bi 2705 . . 3 (¬ ∃𝑦 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑦) = ∅ → (ω ∖ 𝐴) = ∅)
5145, 50syl 17 . 2 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → (ω ∖ 𝐴) = ∅)
52 ssdif0 3776 . 2 (ω ⊆ 𝐴 ↔ (ω ∖ 𝐴) = ∅)
5351, 52sylibr 219 1 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ω ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 378   = wceq 1468  wcel 1937  wne 2675  wral 2791  wrex 2792  cdif 3423  cin 3425  wss 3426  c0 3757  Ord word 5473  suc csuc 5476  ωcom 6769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680  ax-un 6659
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-sbc 3292  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-br 4435  df-opab 4494  df-tr 4531  df-eprel 4791  df-po 4801  df-so 4802  df-fr 4839  df-we 4841  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-om 6770
This theorem is referenced by:  find  6795  finds  6796  finds2  6798  omex  8233  dfom3  8237
  Copyright terms: Public domain W3C validator