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 7796	. 2 ⊢ Ord On
4		trssord 6403	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1460	1 ⊢ Ord ω

Syntax hints:   ⊆ wss 3963  Tr wtr 5265  Ord word 6385  Oncon0 6386  ωcom 7887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390  df-lim 6391  df-om 7888

This theorem is referenced by:  omon  7899  limom  7903  ssnlim  7907  omsindsOLD  7909  peano5  7916  omsucelsucb  8497  nnarcl  8653  nnawordex  8674  oaabslem  8684  oaabs2  8686  omabslem  8687  onomeneqOLD  9264  ominf  9292  ominfOLD  9293  findcard3  9316  findcard3OLD  9317  nnsdomg  9333  nnsdomgOLD  9334  dffi3  9469  wofib  9583  alephgeom  10120  iscard3  10131  iunfictbso  10152  unctb  10242  ackbij2lem1  10256  ackbij1lem3  10259  ackbij1lem18  10274  ackbij2  10280  cflim2  10301  fin23lem26  10363  fin23lem23  10364  fin23lem27  10366  fin67  10433  alephexp1  10617  pwfseqlem3  10698  pwdjundom  10705  winainflem  10731  wunex2  10776  om2uzoi  13993  ltweuz  13999  fz1isolem  14497  1stcrestlem  23476  om2noseqoi  28324  satfn  35340  hfuni  36166  hfninf  36168  finxpreclem4  37377  oaordnrex  43285  omnord1ex  43294  oenord1ex  43305  omabs2  43322  tfsconcat0b  43336  rn1st  45219