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

Theorem peano5OLD 7882
Description: Obsolete version of peano5 7881 as of 3-Oct-2024. (Contributed by NM, 18-Feb-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
peano5OLD ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ω ⊆ 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem peano5OLD
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eldifn 4122 . . . . . 6 (𝑦 ∈ (ω ∖ 𝐴) → ¬ 𝑦𝐴)
21adantl 481 . . . . 5 (((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) → ¬ 𝑦𝐴)
3 eldifi 4121 . . . . . . . 8 (𝑦 ∈ (ω ∖ 𝐴) → 𝑦 ∈ ω)
4 elndif 4123 . . . . . . . . 9 (∅ ∈ 𝐴 → ¬ ∅ ∈ (ω ∖ 𝐴))
5 eleq1 2815 . . . . . . . . . . 11 (𝑦 = ∅ → (𝑦 ∈ (ω ∖ 𝐴) ↔ ∅ ∈ (ω ∖ 𝐴)))
65biimpcd 248 . . . . . . . . . 10 (𝑦 ∈ (ω ∖ 𝐴) → (𝑦 = ∅ → ∅ ∈ (ω ∖ 𝐴)))
76necon3bd 2948 . . . . . . . . 9 (𝑦 ∈ (ω ∖ 𝐴) → (¬ ∅ ∈ (ω ∖ 𝐴) → 𝑦 ≠ ∅))
84, 7mpan9 506 . . . . . . . 8 ((∅ ∈ 𝐴𝑦 ∈ (ω ∖ 𝐴)) → 𝑦 ≠ ∅)
9 nnsuc 7870 . . . . . . . 8 ((𝑦 ∈ ω ∧ 𝑦 ≠ ∅) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥)
103, 8, 9syl2an2 683 . . . . . . 7 ((∅ ∈ 𝐴𝑦 ∈ (ω ∖ 𝐴)) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥)
1110ad4ant13 748 . . . . . 6 ((((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥)
12 nfra1 3275 . . . . . . . . . . 11 𝑥𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)
13 nfv 1909 . . . . . . . . . . 11 𝑥(𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)
1412, 13nfan 1894 . . . . . . . . . 10 𝑥(∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) ∧ (𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅))
15 nfv 1909 . . . . . . . . . 10 𝑥 𝑦𝐴
16 rsp 3238 . . . . . . . . . . 11 (∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴) → (𝑥 ∈ ω → (𝑥𝐴 → suc 𝑥𝐴)))
17 vex 3472 . . . . . . . . . . . . . . . . . 18 𝑥 ∈ V
1817sucid 6440 . . . . . . . . . . . . . . . . 17 𝑥 ∈ suc 𝑥
19 eleq2 2816 . . . . . . . . . . . . . . . . 17 (𝑦 = suc 𝑥 → (𝑥𝑦𝑥 ∈ suc 𝑥))
2018, 19mpbiri 258 . . . . . . . . . . . . . . . 16 (𝑦 = suc 𝑥𝑥𝑦)
21 eleq1 2815 . . . . . . . . . . . . . . . . . 18 (𝑦 = suc 𝑥 → (𝑦 ∈ ω ↔ suc 𝑥 ∈ ω))
22 peano2b 7869 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ω ↔ suc 𝑥 ∈ ω)
2321, 22bitr4di 289 . . . . . . . . . . . . . . . . 17 (𝑦 = suc 𝑥 → (𝑦 ∈ ω ↔ 𝑥 ∈ ω))
24 minel 4460 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑦 ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → ¬ 𝑥 ∈ (ω ∖ 𝐴))
25 neldif 4124 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ω ∧ ¬ 𝑥 ∈ (ω ∖ 𝐴)) → 𝑥𝐴)
2624, 25sylan2 592 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ω ∧ (𝑥𝑦 ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)) → 𝑥𝐴)
2726exp32 420 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ω → (𝑥𝑦 → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → 𝑥𝐴)))
2823, 27biimtrdi 252 . . . . . . . . . . . . . . . 16 (𝑦 = suc 𝑥 → (𝑦 ∈ ω → (𝑥𝑦 → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → 𝑥𝐴))))
2920, 28mpid 44 . . . . . . . . . . . . . . 15 (𝑦 = suc 𝑥 → (𝑦 ∈ ω → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → 𝑥𝐴)))
303, 29syl5 34 . . . . . . . . . . . . . 14 (𝑦 = suc 𝑥 → (𝑦 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → 𝑥𝐴)))
3130impd 410 . . . . . . . . . . . . 13 (𝑦 = suc 𝑥 → ((𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → 𝑥𝐴))
32 eleq1a 2822 . . . . . . . . . . . . . 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 𝑥𝑦𝐴)))
3714, 15, 36rexlimd 3257 . . . . . . . . 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 813 . . . 4 (((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) → ¬ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)
4342nrexdv 3143 . . 3 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ¬ ∃𝑦 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑦) = ∅)
44 ordom 7862 . . . . 5 Ord ω
45 difss 4126 . . . . 5 (ω ∖ 𝐴) ⊆ ω
46 tz7.5 6379 . . . . 5 ((Ord ω ∧ (ω ∖ 𝐴) ⊆ ω ∧ (ω ∖ 𝐴) ≠ ∅) → ∃𝑦 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑦) = ∅)
4744, 45, 46mp3an12 1447 . . . 4 ((ω ∖ 𝐴) ≠ ∅ → ∃𝑦 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑦) = ∅)
4847necon1bi 2963 . . 3 (¬ ∃𝑦 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑦) = ∅ → (ω ∖ 𝐴) = ∅)
4943, 48syl 17 . 2 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → (ω ∖ 𝐴) = ∅)
50 ssdif0 4358 . 2 (ω ⊆ 𝐴 ↔ (ω ∖ 𝐴) = ∅)
5149, 50sylibr 233 1 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ω ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1533  wcel 2098  wne 2934  wral 3055  wrex 3064  cdif 3940  cin 3942  wss 3943  c0 4317  Ord word 6357  suc csuc 6360  ωcom 7852
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-10 2129  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-tr 5259  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-om 7853
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator