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

Theorem peano5 7915
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 7922. (Contributed by NM, 18-Feb-2004.) Avoid ax-10 2141, ax-12 2177. (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 4132 . . . . . 6 (𝑧 ∈ (ω ∖ 𝐴) → ¬ 𝑧𝐴)
21adantl 481 . . . . 5 (((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) → ¬ 𝑧𝐴)
3 eldifi 4131 . . . . . . . 8 (𝑧 ∈ (ω ∖ 𝐴) → 𝑧 ∈ ω)
4 elndif 4133 . . . . . . . . 9 (∅ ∈ 𝐴 → ¬ ∅ ∈ (ω ∖ 𝐴))
5 eleq1 2829 . . . . . . . . . . 11 (𝑧 = ∅ → (𝑧 ∈ (ω ∖ 𝐴) ↔ ∅ ∈ (ω ∖ 𝐴)))
65biimpcd 249 . . . . . . . . . 10 (𝑧 ∈ (ω ∖ 𝐴) → (𝑧 = ∅ → ∅ ∈ (ω ∖ 𝐴)))
76necon3bd 2954 . . . . . . . . 9 (𝑧 ∈ (ω ∖ 𝐴) → (¬ ∅ ∈ (ω ∖ 𝐴) → 𝑧 ≠ ∅))
84, 7mpan9 506 . . . . . . . 8 ((∅ ∈ 𝐴𝑧 ∈ (ω ∖ 𝐴)) → 𝑧 ≠ ∅)
9 nnsuc 7905 . . . . . . . 8 ((𝑧 ∈ ω ∧ 𝑧 ≠ ∅) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
103, 8, 9syl2an2 686 . . . . . . 7 ((∅ ∈ 𝐴𝑧 ∈ (ω ∖ 𝐴)) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
1110ad4ant13 751 . . . . . 6 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦)
12 eleq1w 2824 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
13 suceq 6450 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
1413eleq1d 2826 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (suc 𝑥𝐴 ↔ suc 𝑦𝐴))
1512, 14imbi12d 344 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑥𝐴 → suc 𝑥𝐴) ↔ (𝑦𝐴 → suc 𝑦𝐴)))
1615rspccv 3619 . . . . . . . . . . 11 (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑦 ∈ ω → (𝑦𝐴 → suc 𝑦𝐴)))
17 vex 3484 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
1817sucid 6466 . . . . . . . . . . . . . . . . 17 𝑦 ∈ suc 𝑦
19 eleq2 2830 . . . . . . . . . . . . . . . . 17 (𝑧 = suc 𝑦 → (𝑦𝑧𝑦 ∈ suc 𝑦))
2018, 19mpbiri 258 . . . . . . . . . . . . . . . 16 (𝑧 = suc 𝑦𝑦𝑧)
21 eleq1 2829 . . . . . . . . . . . . . . . . . 18 (𝑧 = suc 𝑦 → (𝑧 ∈ ω ↔ suc 𝑦 ∈ ω))
22 peano2b 7904 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
2321, 22bitr4di 289 . . . . . . . . . . . . . . . . 17 (𝑧 = suc 𝑦 → (𝑧 ∈ ω ↔ 𝑦 ∈ ω))
24 minel 4466 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑧 ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ¬ 𝑦 ∈ (ω ∖ 𝐴))
25 neldif 4134 . . . . . . . . . . . . . . . . . . 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 2836 . . . . . . . . . . . . . 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 3153 . . . . . . . . 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 3149 . . 3 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ¬ ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
44 ordom 7897 . . . . 5 Ord ω
45 difss 4136 . . . . 5 (ω ∖ 𝐴) ⊆ ω
46 tz7.5 6405 . . . . 5 ((Ord ω ∧ (ω ∖ 𝐴) ⊆ ω ∧ (ω ∖ 𝐴) ≠ ∅) → ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4744, 45, 46mp3an12 1453 . . . 4 ((ω ∖ 𝐴) ≠ ∅ → ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅)
4847necon1bi 2969 . . 3 (¬ ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅ → (ω ∖ 𝐴) = ∅)
4943, 48syl 17 . 2 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → (ω ∖ 𝐴) = ∅)
50 ssdif0 4366 . 2 (ω ⊆ 𝐴 ↔ (ω ∖ 𝐴) = ∅)
5149, 50sylibr 234 1 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ω ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1540  wcel 2108  wne 2940  wral 3061  wrex 3070  cdif 3948  cin 3950  wss 3951  c0 4333  Ord word 6383  suc csuc 6386  ωcom 7887
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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-om 7888
This theorem is referenced by:  find  7917  finds  7918  finds2  7920  omex  9683  dfom3  9687
  Copyright terms: Public domain W3C validator