Theorem ordom 7816

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 7815	. 2 ⊢ Tr ω
2		omsson 7810	. 2 ⊢ ω ⊆ On
3		ordon 7720	. 2 ⊢ Ord On
4		trssord 6332	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1463	1 ⊢ Ord ω

Syntax hints:   ⊆ wss 3899  Tr wtr 5203  Ord word 6314  Oncon0 6315  ωcom 7806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-tr 5204  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319  df-lim 6320  df-om 7807

This theorem is referenced by:  omon  7818  limom  7822  ssnlim  7826  peano5  7833  omsucelsucb  8387  nnarcl  8542  nnawordex  8563  oaabslem  8573  oaabs2  8575  omabslem  8576  ominf  9162  findcard3  9181  nnsdomg  9197  tfsnfin2  9261  dffi3  9332  wofib  9448  alephgeom  9990  iscard3  10001  iunfictbso  10022  unctb  10112  ackbij2lem1  10126  ackbij1lem3  10129  ackbij1lem18  10144  ackbij2  10150  cflim2  10171  fin23lem26  10233  fin23lem23  10234  fin23lem27  10236  fin67  10303  alephexp1  10488  pwfseqlem3  10569  pwdjundom  10576  winainflem  10602  wunex2  10647  om2uzoi  13876  ltweuz  13882  fz1isolem  14382  1stcrestlem  23394  om2noseqoi  28264  oldfib  28335  satfn  35498  hfuni  36327  hfninf  36329  finxpreclem4  37538  oaordnrex  43479  omnord1ex  43488  oenord1ex  43499  omabs2  43516  tfsconcat0b  43530  rn1st  45459