Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nnoeomeqom Structured version   Visualization version   GIF version

Theorem nnoeomeqom 41833
Description: Any natural number at least as large as two raised to the power of omega is omega. Lemma 3.25 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.)
Assertion
Ref Expression
nnoeomeqom ((𝐴 ∈ ω ∧ 1o𝐴) → (𝐴o ω) = ω)

Proof of Theorem nnoeomeqom
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 483 . . . 4 ((𝐴 ∈ ω ∧ 1o𝐴) → 𝐴 ∈ ω)
2 nnon 7844 . . . 4 (𝐴 ∈ ω → 𝐴 ∈ On)
31, 2syl 17 . . 3 ((𝐴 ∈ ω ∧ 1o𝐴) → 𝐴 ∈ On)
4 omelon 9623 . . . . 5 ω ∈ On
5 limom 7854 . . . . 5 Lim ω
64, 5pm3.2i 471 . . . 4 (ω ∈ On ∧ Lim ω)
76a1i 11 . . 3 ((𝐴 ∈ ω ∧ 1o𝐴) → (ω ∈ On ∧ Lim ω))
8 0elon 6407 . . . . 5 ∅ ∈ On
98a1i 11 . . . 4 ((𝐴 ∈ ω ∧ 1o𝐴) → ∅ ∈ On)
10 0ss 4392 . . . . 5 ∅ ⊆ 1o
1110a1i 11 . . . 4 ((𝐴 ∈ ω ∧ 1o𝐴) → ∅ ⊆ 1o)
12 simpr 485 . . . 4 ((𝐴 ∈ ω ∧ 1o𝐴) → 1o𝐴)
13 ontr2 6400 . . . . 5 ((∅ ∈ On ∧ 𝐴 ∈ On) → ((∅ ⊆ 1o ∧ 1o𝐴) → ∅ ∈ 𝐴))
1413imp 407 . . . 4 (((∅ ∈ On ∧ 𝐴 ∈ On) ∧ (∅ ⊆ 1o ∧ 1o𝐴)) → ∅ ∈ 𝐴)
159, 3, 11, 12, 14syl22anc 837 . . 3 ((𝐴 ∈ ω ∧ 1o𝐴) → ∅ ∈ 𝐴)
16 oelim 8516 . . 3 (((𝐴 ∈ On ∧ (ω ∈ On ∧ Lim ω)) ∧ ∅ ∈ 𝐴) → (𝐴o ω) = 𝑥 ∈ ω (𝐴o 𝑥))
173, 7, 15, 16syl21anc 836 . 2 ((𝐴 ∈ ω ∧ 1o𝐴) → (𝐴o ω) = 𝑥 ∈ ω (𝐴o 𝑥))
18 ovex 7426 . . . 4 (𝐴o 𝑥) ∈ V
1918dfiun2 5029 . . 3 𝑥 ∈ ω (𝐴o 𝑥) = {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 = (𝐴o 𝑥)}
20 eluniab 4916 . . . . . 6 (𝑧 {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 = (𝐴o 𝑥)} ↔ ∃𝑦(𝑧𝑦 ∧ ∃𝑥 ∈ ω 𝑦 = (𝐴o 𝑥)))
21 19.42v 1957 . . . . . . . 8 (∃𝑥(𝑧𝑦 ∧ (𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥))) ↔ (𝑧𝑦 ∧ ∃𝑥(𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥))))
22 3anass 1095 . . . . . . . . 9 ((𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)) ↔ (𝑧𝑦 ∧ (𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥))))
2322exbii 1850 . . . . . . . 8 (∃𝑥(𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)) ↔ ∃𝑥(𝑧𝑦 ∧ (𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥))))
24 df-rex 3070 . . . . . . . . 9 (∃𝑥 ∈ ω 𝑦 = (𝐴o 𝑥) ↔ ∃𝑥(𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)))
2524anbi2i 623 . . . . . . . 8 ((𝑧𝑦 ∧ ∃𝑥 ∈ ω 𝑦 = (𝐴o 𝑥)) ↔ (𝑧𝑦 ∧ ∃𝑥(𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥))))
2621, 23, 253bitr4ri 303 . . . . . . 7 ((𝑧𝑦 ∧ ∃𝑥 ∈ ω 𝑦 = (𝐴o 𝑥)) ↔ ∃𝑥(𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)))
2726exbii 1850 . . . . . 6 (∃𝑦(𝑧𝑦 ∧ ∃𝑥 ∈ ω 𝑦 = (𝐴o 𝑥)) ↔ ∃𝑦𝑥(𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)))
28 excom 2162 . . . . . 6 (∃𝑦𝑥(𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)) ↔ ∃𝑥𝑦(𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)))
2920, 27, 283bitri 296 . . . . 5 (𝑧 {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 = (𝐴o 𝑥)} ↔ ∃𝑥𝑦(𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)))
30 simpr3 1196 . . . . . . . . . 10 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ (𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥))) → 𝑦 = (𝐴o 𝑥))
31 simp2 1137 . . . . . . . . . . . 12 ((𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)) → 𝑥 ∈ ω)
32 nnecl 8596 . . . . . . . . . . . 12 ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴o 𝑥) ∈ ω)
331, 31, 32syl2an 596 . . . . . . . . . . 11 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ (𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥))) → (𝐴o 𝑥) ∈ ω)
34 onelss 6395 . . . . . . . . . . 11 (ω ∈ On → ((𝐴o 𝑥) ∈ ω → (𝐴o 𝑥) ⊆ ω))
354, 33, 34mpsyl 68 . . . . . . . . . 10 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ (𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥))) → (𝐴o 𝑥) ⊆ ω)
3630, 35eqsstrd 4016 . . . . . . . . 9 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ (𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥))) → 𝑦 ⊆ ω)
37 simpr1 1194 . . . . . . . . 9 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ (𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥))) → 𝑧𝑦)
3836, 37sseldd 3979 . . . . . . . 8 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ (𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥))) → 𝑧 ∈ ω)
3938ex 413 . . . . . . 7 ((𝐴 ∈ ω ∧ 1o𝐴) → ((𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)) → 𝑧 ∈ ω))
4039exlimdvv 1937 . . . . . 6 ((𝐴 ∈ ω ∧ 1o𝐴) → (∃𝑥𝑦(𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)) → 𝑧 ∈ ω))
41 peano2 7863 . . . . . . . . 9 (𝑧 ∈ ω → suc 𝑧 ∈ ω)
4241adantl 482 . . . . . . . 8 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ 𝑧 ∈ ω) → suc 𝑧 ∈ ω)
43 ovex 7426 . . . . . . . . . 10 (𝐴o suc 𝑧) ∈ V
4443a1i 11 . . . . . . . . 9 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ 𝑧 ∈ ω) → (𝐴o suc 𝑧) ∈ V)
452anim1i 615 . . . . . . . . . . . . 13 ((𝐴 ∈ ω ∧ 1o𝐴) → (𝐴 ∈ On ∧ 1o𝐴))
46 ondif2 8484 . . . . . . . . . . . . 13 (𝐴 ∈ (On ∖ 2o) ↔ (𝐴 ∈ On ∧ 1o𝐴))
4745, 46sylibr 233 . . . . . . . . . . . 12 ((𝐴 ∈ ω ∧ 1o𝐴) → 𝐴 ∈ (On ∖ 2o))
48 nnon 7844 . . . . . . . . . . . . 13 (suc 𝑧 ∈ ω → suc 𝑧 ∈ On)
4941, 48syl 17 . . . . . . . . . . . 12 (𝑧 ∈ ω → suc 𝑧 ∈ On)
50 oeworde 8576 . . . . . . . . . . . 12 ((𝐴 ∈ (On ∖ 2o) ∧ suc 𝑧 ∈ On) → suc 𝑧 ⊆ (𝐴o suc 𝑧))
5147, 49, 50syl2an 596 . . . . . . . . . . 11 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ 𝑧 ∈ ω) → suc 𝑧 ⊆ (𝐴o suc 𝑧))
52 vex 3477 . . . . . . . . . . . . 13 𝑧 ∈ V
5352sucid 6435 . . . . . . . . . . . 12 𝑧 ∈ suc 𝑧
5453a1i 11 . . . . . . . . . . 11 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ 𝑧 ∈ ω) → 𝑧 ∈ suc 𝑧)
5551, 54sseldd 3979 . . . . . . . . . 10 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ 𝑧 ∈ ω) → 𝑧 ∈ (𝐴o suc 𝑧))
56 eqidd 2732 . . . . . . . . . 10 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ 𝑧 ∈ ω) → (𝐴o suc 𝑧) = (𝐴o suc 𝑧))
5755, 42, 563jca 1128 . . . . . . . . 9 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ 𝑧 ∈ ω) → (𝑧 ∈ (𝐴o suc 𝑧) ∧ suc 𝑧 ∈ ω ∧ (𝐴o suc 𝑧) = (𝐴o suc 𝑧)))
58 eleq2 2821 . . . . . . . . . 10 (𝑦 = (𝐴o suc 𝑧) → (𝑧𝑦𝑧 ∈ (𝐴o suc 𝑧)))
59 eqeq1 2735 . . . . . . . . . 10 (𝑦 = (𝐴o suc 𝑧) → (𝑦 = (𝐴o suc 𝑧) ↔ (𝐴o suc 𝑧) = (𝐴o suc 𝑧)))
6058, 593anbi13d 1438 . . . . . . . . 9 (𝑦 = (𝐴o suc 𝑧) → ((𝑧𝑦 ∧ suc 𝑧 ∈ ω ∧ 𝑦 = (𝐴o suc 𝑧)) ↔ (𝑧 ∈ (𝐴o suc 𝑧) ∧ suc 𝑧 ∈ ω ∧ (𝐴o suc 𝑧) = (𝐴o suc 𝑧))))
6144, 57, 60spcedv 3585 . . . . . . . 8 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ 𝑧 ∈ ω) → ∃𝑦(𝑧𝑦 ∧ suc 𝑧 ∈ ω ∧ 𝑦 = (𝐴o suc 𝑧)))
62 eleq1 2820 . . . . . . . . . 10 (𝑥 = suc 𝑧 → (𝑥 ∈ ω ↔ suc 𝑧 ∈ ω))
63 oveq2 7401 . . . . . . . . . . 11 (𝑥 = suc 𝑧 → (𝐴o 𝑥) = (𝐴o suc 𝑧))
6463eqeq2d 2742 . . . . . . . . . 10 (𝑥 = suc 𝑧 → (𝑦 = (𝐴o 𝑥) ↔ 𝑦 = (𝐴o suc 𝑧)))
6562, 643anbi23d 1439 . . . . . . . . 9 (𝑥 = suc 𝑧 → ((𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)) ↔ (𝑧𝑦 ∧ suc 𝑧 ∈ ω ∧ 𝑦 = (𝐴o suc 𝑧))))
6665exbidv 1924 . . . . . . . 8 (𝑥 = suc 𝑧 → (∃𝑦(𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)) ↔ ∃𝑦(𝑧𝑦 ∧ suc 𝑧 ∈ ω ∧ 𝑦 = (𝐴o suc 𝑧))))
6742, 61, 66spcedv 3585 . . . . . . 7 (((𝐴 ∈ ω ∧ 1o𝐴) ∧ 𝑧 ∈ ω) → ∃𝑥𝑦(𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)))
6867ex 413 . . . . . 6 ((𝐴 ∈ ω ∧ 1o𝐴) → (𝑧 ∈ ω → ∃𝑥𝑦(𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥))))
6940, 68impbid 211 . . . . 5 ((𝐴 ∈ ω ∧ 1o𝐴) → (∃𝑥𝑦(𝑧𝑦𝑥 ∈ ω ∧ 𝑦 = (𝐴o 𝑥)) ↔ 𝑧 ∈ ω))
7029, 69bitrid 282 . . . 4 ((𝐴 ∈ ω ∧ 1o𝐴) → (𝑧 {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 = (𝐴o 𝑥)} ↔ 𝑧 ∈ ω))
7170eqrdv 2729 . . 3 ((𝐴 ∈ ω ∧ 1o𝐴) → {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 = (𝐴o 𝑥)} = ω)
7219, 71eqtrid 2783 . 2 ((𝐴 ∈ ω ∧ 1o𝐴) → 𝑥 ∈ ω (𝐴o 𝑥) = ω)
7317, 72eqtrd 2771 1 ((𝐴 ∈ ω ∧ 1o𝐴) → (𝐴o ω) = ω)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  {cab 2708  wrex 3069  Vcvv 3473  cdif 3941  wss 3944  c0 4318   cuni 4901   ciun 4990  Oncon0 6353  Lim wlim 6354  suc csuc 6355  (class class class)co 7393  ωcom 7838  1oc1o 8441  2oc2o 8442  o coe 8447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7708  ax-inf2 9618
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-ov 7396  df-oprab 7397  df-mpo 7398  df-om 7839  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-1o 8448  df-2o 8449  df-oadd 8452  df-omul 8453  df-oexp 8454
This theorem is referenced by:  oenord1ex  41836  oaomoencom  41838
  Copyright terms: Public domain W3C validator