Theorem ordom 7913

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 7912	. 2 ⊢ Tr ω
2		omsson 7907	. 2 ⊢ ω ⊆ On
3		ordon 7812	. 2 ⊢ Ord On
4		trssord 6412	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1461	1 ⊢ Ord ω

Syntax hints:   ⊆ wss 3976  Tr wtr 5283  Ord word 6394  Oncon0 6395  ωcom 7903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399  df-lim 6400  df-om 7904

This theorem is referenced by:  omon  7915  limom  7919  ssnlim  7923  omsindsOLD  7925  peano5  7932  peano5OLD  7933  omsucelsucb  8514  nnarcl  8672  nnawordex  8693  oaabslem  8703  oaabs2  8705  omabslem  8706  onomeneqOLD  9292  ominf  9321  ominfOLD  9322  findcard3  9346  findcard3OLD  9347  nnsdomg  9363  nnsdomgOLD  9364  dffi3  9500  wofib  9614  alephgeom  10151  iscard3  10162  iunfictbso  10183  unctb  10273  ackbij2lem1  10287  ackbij1lem3  10290  ackbij1lem18  10305  ackbij2  10311  cflim2  10332  fin23lem26  10394  fin23lem23  10395  fin23lem27  10397  fin67  10464  alephexp1  10648  pwfseqlem3  10729  pwdjundom  10736  winainflem  10762  wunex2  10807  om2uzoi  14006  ltweuz  14012  fz1isolem  14510  1stcrestlem  23481  om2noseqoi  28327  satfn  35323  hfuni  36148  hfninf  36150  finxpreclem4  37360  oaordnrex  43257  omnord1ex  43266  oenord1ex  43277  omabs2  43294  tfsconcat0b  43308  rn1st  45183