Theorem ordom 7897

Description: The class of finite ordinals ω is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43. Theorem 1.22 of [Schloeder] p. 3. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
ordom	⊢ Ord ω

Proof of Theorem ordom

Step	Hyp	Ref	Expression
1		trom 7896	. 2 ⊢ Tr ω
2		omsson 7891	. 2 ⊢ ω ⊆ On
3		ordon 7797	. 2 ⊢ Ord On
4		trssord 6401	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1463	1 ⊢ Ord ω

Syntax hints:   ⊆ wss 3951  Tr wtr 5259  Ord word 6383  Oncon0 6384  ωcom 7887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-lim 6389  df-om 7888

This theorem is referenced by:  omon  7899  limom  7903  ssnlim  7907  peano5  7915  omsucelsucb  8498  nnarcl  8654  nnawordex  8675  oaabslem  8685  oaabs2  8687  omabslem  8688  onomeneqOLD  9266  ominf  9294  ominfOLD  9295  findcard3  9318  findcard3OLD  9319  nnsdomg  9335  nnsdomgOLD  9336  dffi3  9471  wofib  9585  alephgeom  10122  iscard3  10133  iunfictbso  10154  unctb  10244  ackbij2lem1  10258  ackbij1lem3  10261  ackbij1lem18  10276  ackbij2  10282  cflim2  10303  fin23lem26  10365  fin23lem23  10366  fin23lem27  10368  fin67  10435  alephexp1  10619  pwfseqlem3  10700  pwdjundom  10707  winainflem  10733  wunex2  10778  om2uzoi  13996  ltweuz  14002  fz1isolem  14500  1stcrestlem  23460  om2noseqoi  28309  satfn  35360  hfuni  36185  hfninf  36187  finxpreclem4  37395  oaordnrex  43308  omnord1ex  43317  oenord1ex  43328  omabs2  43345  tfsconcat0b  43359  rn1st  45280