Theorem ordom 7828

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 7827	. 2 ⊢ Tr ω
2		omsson 7822	. 2 ⊢ ω ⊆ On
3		ordon 7732	. 2 ⊢ Ord On
4		trssord 6342	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1464	1 ⊢ Ord ω

Syntax hints:   ⊆ wss 3903  Tr wtr 5207  Ord word 6324  Oncon0 6325  ωcom 7818

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-on 6329  df-lim 6330  df-om 7819

This theorem is referenced by:  omon  7830  limom  7834  ssnlim  7838  peano5  7845  omsucelsucb  8399  nnarcl  8554  nnawordex  8575  oaabslem  8585  oaabs2  8587  omabslem  8588  ominf  9176  findcard3  9195  nnsdomg  9211  tfsnfin2  9275  dffi3  9346  wofib  9462  alephgeom  10004  iscard3  10015  iunfictbso  10036  unctb  10126  ackbij2lem1  10140  ackbij1lem3  10143  ackbij1lem18  10158  ackbij2  10164  cflim2  10185  fin23lem26  10247  fin23lem23  10248  fin23lem27  10250  fin67  10317  alephexp1  10502  pwfseqlem3  10583  pwdjundom  10590  winainflem  10616  wunex2  10661  om2uzoi  13890  ltweuz  13896  fz1isolem  14396  1stcrestlem  23408  om2noseqoi  28311  oldfib  28385  z12bdaylem  28492  satfn  35571  hfuni  36400  hfninf  36402  finxpreclem4  37649  oaordnrex  43652  omnord1ex  43661  oenord1ex  43672  omabs2  43689  tfsconcat0b  43703  rn1st  45631