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

Theorem ordom 7220
 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 4886 . . 3 (Tr ω ↔ ∀𝑦𝑥((𝑦𝑥𝑥 ∈ ω) → 𝑦 ∈ ω))
2 onelon 5891 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
32expcom 398 . . . . . . 7 (𝑦𝑥 → (𝑥 ∈ On → 𝑦 ∈ On))
4 limord 5927 . . . . . . . . . . . 12 (Lim 𝑧 → Ord 𝑧)
5 ordtr 5880 . . . . . . . . . . . 12 (Ord 𝑧 → Tr 𝑧)
6 trel 4891 . . . . . . . . . . . 12 (Tr 𝑧 → ((𝑦𝑥𝑥𝑧) → 𝑦𝑧))
74, 5, 63syl 18 . . . . . . . . . . 11 (Lim 𝑧 → ((𝑦𝑥𝑥𝑧) → 𝑦𝑧))
87expd 400 . . . . . . . . . 10 (Lim 𝑧 → (𝑦𝑥 → (𝑥𝑧𝑦𝑧)))
98com12 32 . . . . . . . . 9 (𝑦𝑥 → (Lim 𝑧 → (𝑥𝑧𝑦𝑧)))
109a2d 29 . . . . . . . 8 (𝑦𝑥 → ((Lim 𝑧𝑥𝑧) → (Lim 𝑧𝑦𝑧)))
1110alimdv 1996 . . . . . . 7 (𝑦𝑥 → (∀𝑧(Lim 𝑧𝑥𝑧) → ∀𝑧(Lim 𝑧𝑦𝑧)))
123, 11anim12d 588 . . . . . 6 (𝑦𝑥 → ((𝑥 ∈ On ∧ ∀𝑧(Lim 𝑧𝑥𝑧)) → (𝑦 ∈ On ∧ ∀𝑧(Lim 𝑧𝑦𝑧))))
13 elom 7214 . . . . . 6 (𝑥 ∈ ω ↔ (𝑥 ∈ On ∧ ∀𝑧(Lim 𝑧𝑥𝑧)))
14 elom 7214 . . . . . 6 (𝑦 ∈ ω ↔ (𝑦 ∈ On ∧ ∀𝑧(Lim 𝑧𝑦𝑧)))
1512, 13, 143imtr4g 285 . . . . 5 (𝑦𝑥 → (𝑥 ∈ ω → 𝑦 ∈ ω))
1615imp 393 . . . 4 ((𝑦𝑥𝑥 ∈ ω) → 𝑦 ∈ ω)
1716ax-gen 1869 . . 3 𝑥((𝑦𝑥𝑥 ∈ ω) → 𝑦 ∈ ω)
181, 17mpgbir 1873 . 2 Tr ω
19 omsson 7215 . 2 ω ⊆ On
20 ordon 7128 . 2 Ord On
21 trssord 5883 . 2 ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
2218, 19, 20, 21mp3an 1571 1 Ord ω
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 382  ∀wal 1628   ∈ wcel 2144   ⊆ wss 3721  Tr wtr 4884  Ord word 5865  Oncon0 5866  Lim wlim 5867  ωcom 7211 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pr 5034  ax-un 7095 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-br 4785  df-opab 4845  df-tr 4885  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-om 7212 This theorem is referenced by:  elnn  7221  omon  7222  limom  7226  ssnlim  7229  omsinds  7230  peano5  7235  nnarcl  7849  nnawordex  7870  oaabslem  7876  oaabs2  7878  omabslem  7879  onomeneq  8305  ominf  8327  findcard3  8358  nnsdomg  8374  dffi3  8492  wofib  8605  alephgeom  9104  iscard3  9115  iunfictbso  9136  unctb  9228  ackbij2lem1  9242  ackbij1lem3  9245  ackbij1lem18  9260  ackbij2  9266  cflim2  9286  fin23lem26  9348  fin23lem23  9349  fin23lem27  9351  fin67  9418  alephexp1  9602  pwfseqlem3  9683  pwcdandom  9690  winainflem  9716  wunex2  9761  om2uzoi  12961  ltweuz  12967  fz1isolem  13446  1stcrestlem  21475  hfuni  32622  hfninf  32624  finxpreclem4  33561
 Copyright terms: Public domain W3C validator