Theorem ordom 7817

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 7816	. 2 ⊢ Tr ω
2		omsson 7811	. 2 ⊢ ω ⊆ On
3		ordon 7716	. 2 ⊢ Ord On
4		trssord 6339	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1461	1 ⊢ Ord ω

Syntax hints:   ⊆ wss 3913  Tr wtr 5227  Ord word 6321  Oncon0 6322  ωcom 7807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-tr 5228  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-ord 6325  df-on 6326  df-lim 6327  df-om 7808

This theorem is referenced by:  omon  7819  limom  7823  ssnlim  7827  omsindsOLD  7829  peano5  7835  peano5OLD  7836  omsucelsucb  8409  nnarcl  8568  nnawordex  8589  oaabslem  8598  oaabs2  8600  omabslem  8601  onomeneqOLD  9180  ominf  9209  ominfOLD  9210  findcard3  9236  findcard3OLD  9237  nnsdomg  9253  nnsdomgOLD  9254  dffi3  9376  wofib  9490  alephgeom  10027  iscard3  10038  iunfictbso  10059  unctb  10150  ackbij2lem1  10164  ackbij1lem3  10167  ackbij1lem18  10182  ackbij2  10188  cflim2  10208  fin23lem26  10270  fin23lem23  10271  fin23lem27  10273  fin67  10340  alephexp1  10524  pwfseqlem3  10605  pwdjundom  10612  winainflem  10638  wunex2  10683  om2uzoi  13870  ltweuz  13876  fz1isolem  14372  1stcrestlem  22840  satfn  34036  hfuni  34845  hfninf  34847  finxpreclem4  35938  oaordnrex  41688  omnord1ex  41697  oenord1ex  41708  omabs2  41725  tfsconcat0b  41739  rn1st  43623