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

Theorem ordom 7405
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 5032 . . 3 (Tr ω ↔ ∀𝑦𝑥((𝑦𝑥𝑥 ∈ ω) → 𝑦 ∈ ω))
2 onelon 6054 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
32expcom 406 . . . . . . 7 (𝑦𝑥 → (𝑥 ∈ On → 𝑦 ∈ On))
4 limord 6088 . . . . . . . . . . . 12 (Lim 𝑧 → Ord 𝑧)
5 ordtr 6043 . . . . . . . . . . . 12 (Ord 𝑧 → Tr 𝑧)
6 trel 5037 . . . . . . . . . . . 12 (Tr 𝑧 → ((𝑦𝑥𝑥𝑧) → 𝑦𝑧))
74, 5, 63syl 18 . . . . . . . . . . 11 (Lim 𝑧 → ((𝑦𝑥𝑥𝑧) → 𝑦𝑧))
87expd 408 . . . . . . . . . 10 (Lim 𝑧 → (𝑦𝑥 → (𝑥𝑧𝑦𝑧)))
98com12 32 . . . . . . . . 9 (𝑦𝑥 → (Lim 𝑧 → (𝑥𝑧𝑦𝑧)))
109a2d 29 . . . . . . . 8 (𝑦𝑥 → ((Lim 𝑧𝑥𝑧) → (Lim 𝑧𝑦𝑧)))
1110alimdv 1875 . . . . . . 7 (𝑦𝑥 → (∀𝑧(Lim 𝑧𝑥𝑧) → ∀𝑧(Lim 𝑧𝑦𝑧)))
123, 11anim12d 599 . . . . . 6 (𝑦𝑥 → ((𝑥 ∈ On ∧ ∀𝑧(Lim 𝑧𝑥𝑧)) → (𝑦 ∈ On ∧ ∀𝑧(Lim 𝑧𝑦𝑧))))
13 elom 7399 . . . . . 6 (𝑥 ∈ ω ↔ (𝑥 ∈ On ∧ ∀𝑧(Lim 𝑧𝑥𝑧)))
14 elom 7399 . . . . . 6 (𝑦 ∈ ω ↔ (𝑦 ∈ On ∧ ∀𝑧(Lim 𝑧𝑦𝑧)))
1512, 13, 143imtr4g 288 . . . . 5 (𝑦𝑥 → (𝑥 ∈ ω → 𝑦 ∈ ω))
1615imp 398 . . . 4 ((𝑦𝑥𝑥 ∈ ω) → 𝑦 ∈ ω)
1716ax-gen 1758 . . 3 𝑥((𝑦𝑥𝑥 ∈ ω) → 𝑦 ∈ ω)
181, 17mpgbir 1762 . 2 Tr ω
19 omsson 7400 . 2 ω ⊆ On
20 ordon 7314 . 2 Ord On
21 trssord 6046 . 2 ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
2218, 19, 20, 21mp3an 1440 1 Ord ω
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  wal 1505  wcel 2050  wss 3829  Tr wtr 5030  Ord word 6028  Oncon0 6029  Lim wlim 6030  ωcom 7396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pr 5186  ax-un 7279
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3682  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-tr 5031  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-om 7397
This theorem is referenced by:  elnn  7406  omon  7407  limom  7411  ssnlim  7414  omsinds  7415  peano5  7420  omsucelsucb  7897  nnarcl  8043  nnawordex  8064  oaabslem  8070  oaabs2  8072  omabslem  8073  onomeneq  8503  ominf  8525  findcard3  8556  nnsdomg  8572  dffi3  8690  wofib  8804  alephgeom  9302  iscard3  9313  iunfictbso  9334  unctb  9425  ackbij2lem1  9439  ackbij1lem3  9442  ackbij1lem18  9457  ackbij2  9463  cflim2  9483  fin23lem26  9545  fin23lem23  9546  fin23lem27  9548  fin67  9615  alephexp1  9799  pwfseqlem3  9880  pwdjundom  9887  winainflem  9913  wunex2  9958  om2uzoi  13138  ltweuz  13144  fz1isolem  13632  1stcrestlem  21764  hfuni  33172  hfninf  33174  finxpreclem4  34122
  Copyright terms: Public domain W3C validator