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

Theorem ordom 7578
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 5165 . . 3 (Tr ω ↔ ∀𝑦𝑥((𝑦𝑥𝑥 ∈ ω) → 𝑦 ∈ ω))
2 onelon 6209 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
32expcom 414 . . . . . . 7 (𝑦𝑥 → (𝑥 ∈ On → 𝑦 ∈ On))
4 limord 6243 . . . . . . . . . . . 12 (Lim 𝑧 → Ord 𝑧)
5 ordtr 6198 . . . . . . . . . . . 12 (Ord 𝑧 → Tr 𝑧)
6 trel 5170 . . . . . . . . . . . 12 (Tr 𝑧 → ((𝑦𝑥𝑥𝑧) → 𝑦𝑧))
74, 5, 63syl 18 . . . . . . . . . . 11 (Lim 𝑧 → ((𝑦𝑥𝑥𝑧) → 𝑦𝑧))
87expd 416 . . . . . . . . . 10 (Lim 𝑧 → (𝑦𝑥 → (𝑥𝑧𝑦𝑧)))
98com12 32 . . . . . . . . 9 (𝑦𝑥 → (Lim 𝑧 → (𝑥𝑧𝑦𝑧)))
109a2d 29 . . . . . . . 8 (𝑦𝑥 → ((Lim 𝑧𝑥𝑧) → (Lim 𝑧𝑦𝑧)))
1110alimdv 1908 . . . . . . 7 (𝑦𝑥 → (∀𝑧(Lim 𝑧𝑥𝑧) → ∀𝑧(Lim 𝑧𝑦𝑧)))
123, 11anim12d 608 . . . . . 6 (𝑦𝑥 → ((𝑥 ∈ On ∧ ∀𝑧(Lim 𝑧𝑥𝑧)) → (𝑦 ∈ On ∧ ∀𝑧(Lim 𝑧𝑦𝑧))))
13 elom 7572 . . . . . 6 (𝑥 ∈ ω ↔ (𝑥 ∈ On ∧ ∀𝑧(Lim 𝑧𝑥𝑧)))
14 elom 7572 . . . . . 6 (𝑦 ∈ ω ↔ (𝑦 ∈ On ∧ ∀𝑧(Lim 𝑧𝑦𝑧)))
1512, 13, 143imtr4g 297 . . . . 5 (𝑦𝑥 → (𝑥 ∈ ω → 𝑦 ∈ ω))
1615imp 407 . . . 4 ((𝑦𝑥𝑥 ∈ ω) → 𝑦 ∈ ω)
1716ax-gen 1787 . . 3 𝑥((𝑦𝑥𝑥 ∈ ω) → 𝑦 ∈ ω)
181, 17mpgbir 1791 . 2 Tr ω
19 omsson 7573 . 2 ω ⊆ On
20 ordon 7487 . 2 Ord On
21 trssord 6201 . 2 ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
2218, 19, 20, 21mp3an 1452 1 Ord ω
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wal 1526  wcel 2105  wss 3933  Tr wtr 5163  Ord word 6183  Oncon0 6184  Lim wlim 6185  ωcom 7569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-tr 5164  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-om 7570
This theorem is referenced by:  elnn  7579  omon  7580  limom  7584  ssnlim  7588  omsinds  7589  peano5  7594  omsucelsucb  8083  nnarcl  8231  nnawordex  8252  oaabslem  8259  oaabs2  8261  omabslem  8262  onomeneq  8696  ominf  8718  findcard3  8749  nnsdomg  8765  dffi3  8883  wofib  8997  alephgeom  9496  iscard3  9507  iunfictbso  9528  unctb  9615  ackbij2lem1  9629  ackbij1lem3  9632  ackbij1lem18  9647  ackbij2  9653  cflim2  9673  fin23lem26  9735  fin23lem23  9736  fin23lem27  9738  fin67  9805  alephexp1  9989  pwfseqlem3  10070  pwdjundom  10077  winainflem  10103  wunex2  10148  om2uzoi  13311  ltweuz  13317  fz1isolem  13807  1stcrestlem  21988  satfn  32499  hfuni  33542  hfninf  33544  finxpreclem4  34557
  Copyright terms: Public domain W3C validator