Theorem ordom 7856

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 7855	. 2 ⊢ Tr ω
2		omsson 7850	. 2 ⊢ ω ⊆ On
3		ordon 7760	. 2 ⊢ Ord On
4		trssord 6363	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1482	1 ⊢ Ord ω

Syntax hints:   ⊆ wss 3904  Tr wtr 5207  Ord word 6345  Oncon0 6346  ωcom 7846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-ord 6349  df-on 6350  df-lim 6351  df-om 7847

This theorem is referenced by:  omon  7858  limom  7862  ssnlim  7866  peano5  7874  omsucelsucb  8429  nnarcl  8586  nnawordex  8607  oaabslem  8617  oaabs2  8619  omabslem  8620  ominf  9208  findcard3  9227  nnsdomg  9243  tfsnfin2  9306  dffi3  9377  wofib  9493  alephgeom  10038  iscard3  10049  iunfictbso  10070  unctb  10160  ackbij2lem1  10174  ackbij1lem3  10177  ackbij1lem18  10192  ackbij2  10198  cflim2  10220  fin23lem26  10282  fin23lem23  10283  fin23lem27  10285  fin67  10352  alephexp1  10537  pwfseqlem3  10618  pwdjundom  10625  winainflem  10651  wunex2  10696  om2uzoi  13968  ltweuz  13974  fz1isolem  14474  1stcrestlem  23512  om2noseqoi  28396  oldfib  28470  z12bdaylem  28577  satfn  35705  hfuni  36534  hfninf  36536  bj-iomnnom  37751  finxpreclem4  37888  oaordnrex  43872  omnord1ex  43881  oenord1ex  43892  omabs2  43909  tfsconcat0b  43923  rn1st  45848