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

Theorem ordom 7028
 Description: Omega is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
ordom Ord ω

Proof of Theorem ordom
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dftr2 4719 . . 3 (Tr ω ↔ ∀𝑦𝑥((𝑦𝑥𝑥 ∈ ω) → 𝑦 ∈ ω))
2 onelon 5712 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
32expcom 451 . . . . . . 7 (𝑦𝑥 → (𝑥 ∈ On → 𝑦 ∈ On))
4 limord 5748 . . . . . . . . . . . 12 (Lim 𝑧 → Ord 𝑧)
5 ordtr 5701 . . . . . . . . . . . 12 (Ord 𝑧 → Tr 𝑧)
6 trel 4724 . . . . . . . . . . . 12 (Tr 𝑧 → ((𝑦𝑥𝑥𝑧) → 𝑦𝑧))
74, 5, 63syl 18 . . . . . . . . . . 11 (Lim 𝑧 → ((𝑦𝑥𝑥𝑧) → 𝑦𝑧))
87expd 452 . . . . . . . . . 10 (Lim 𝑧 → (𝑦𝑥 → (𝑥𝑧𝑦𝑧)))
98com12 32 . . . . . . . . 9 (𝑦𝑥 → (Lim 𝑧 → (𝑥𝑧𝑦𝑧)))
109a2d 29 . . . . . . . 8 (𝑦𝑥 → ((Lim 𝑧𝑥𝑧) → (Lim 𝑧𝑦𝑧)))
1110alimdv 1842 . . . . . . 7 (𝑦𝑥 → (∀𝑧(Lim 𝑧𝑥𝑧) → ∀𝑧(Lim 𝑧𝑦𝑧)))
123, 11anim12d 585 . . . . . 6 (𝑦𝑥 → ((𝑥 ∈ On ∧ ∀𝑧(Lim 𝑧𝑥𝑧)) → (𝑦 ∈ On ∧ ∀𝑧(Lim 𝑧𝑦𝑧))))
13 elom 7022 . . . . . 6 (𝑥 ∈ ω ↔ (𝑥 ∈ On ∧ ∀𝑧(Lim 𝑧𝑥𝑧)))
14 elom 7022 . . . . . 6 (𝑦 ∈ ω ↔ (𝑦 ∈ On ∧ ∀𝑧(Lim 𝑧𝑦𝑧)))
1512, 13, 143imtr4g 285 . . . . 5 (𝑦𝑥 → (𝑥 ∈ ω → 𝑦 ∈ ω))
1615imp 445 . . . 4 ((𝑦𝑥𝑥 ∈ ω) → 𝑦 ∈ ω)
1716ax-gen 1719 . . 3 𝑥((𝑦𝑥𝑥 ∈ ω) → 𝑦 ∈ ω)
181, 17mpgbir 1723 . 2 Tr ω
19 omsson 7023 . 2 ω ⊆ On
20 ordon 6936 . 2 Ord On
21 trssord 5704 . 2 ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
2218, 19, 20, 21mp3an 1421 1 Ord ω
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384  ∀wal 1478   ∈ wcel 1987   ⊆ wss 3559  Tr wtr 4717  Ord word 5686  Oncon0 5687  Lim wlim 5688  ωcom 7019 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6909 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-tr 4718  df-eprel 4990  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-om 7020 This theorem is referenced by:  elnn  7029  omon  7030  limom  7034  ssnlim  7037  omsinds  7038  peano5  7043  nnarcl  7648  nnawordex  7669  oaabslem  7675  oaabs2  7677  omabslem  7678  onomeneq  8101  ominf  8123  findcard3  8154  nnsdomg  8170  dffi3  8288  wofib  8401  alephgeom  8856  iscard3  8867  iunfictbso  8888  unctb  8978  ackbij2lem1  8992  ackbij1lem3  8995  ackbij1lem18  9010  ackbij2  9016  cflim2  9036  fin23lem26  9098  fin23lem23  9099  fin23lem27  9101  fin67  9168  alephexp1  9352  pwfseqlem3  9433  pwcdandom  9440  winainflem  9466  wunex2  9511  om2uzoi  12701  ltweuz  12707  fz1isolem  13190  mreexexdOLD  16237  1stcrestlem  21174  hfuni  31960  hfninf  31962  finxpreclem4  32890
 Copyright terms: Public domain W3C validator