Theorem ordom 7855

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 7854	. 2 ⊢ Tr ω
2		omsson 7849	. 2 ⊢ ω ⊆ On
3		ordon 7756	. 2 ⊢ Ord On
4		trssord 6352	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1463	1 ⊢ Ord ω

Syntax hints:   ⊆ wss 3917  Tr wtr 5217  Ord word 6334  Oncon0 6335  ωcom 7845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339  df-lim 6340  df-om 7846

This theorem is referenced by:  omon  7857  limom  7861  ssnlim  7865  peano5  7872  omsucelsucb  8429  nnarcl  8583  nnawordex  8604  oaabslem  8614  oaabs2  8616  omabslem  8617  ominf  9212  ominfOLD  9213  findcard3  9236  findcard3OLD  9237  nnsdomg  9253  nnsdomgOLD  9254  dffi3  9389  wofib  9505  alephgeom  10042  iscard3  10053  iunfictbso  10074  unctb  10164  ackbij2lem1  10178  ackbij1lem3  10181  ackbij1lem18  10196  ackbij2  10202  cflim2  10223  fin23lem26  10285  fin23lem23  10286  fin23lem27  10288  fin67  10355  alephexp1  10539  pwfseqlem3  10620  pwdjundom  10627  winainflem  10653  wunex2  10698  om2uzoi  13927  ltweuz  13933  fz1isolem  14433  1stcrestlem  23346  om2noseqoi  28204  satfn  35349  hfuni  36179  hfninf  36181  finxpreclem4  37389  oaordnrex  43291  omnord1ex  43300  oenord1ex  43311  omabs2  43328  tfsconcat0b  43342  rn1st  45274