Theorem ordom 7865

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 7864	. 2 ⊢ Tr ω
2		omsson 7859	. 2 ⊢ ω ⊆ On
3		ordon 7764	. 2 ⊢ Ord On
4		trssord 6382	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1462	1 ⊢ Ord ω

Syntax hints:   ⊆ wss 3949  Tr wtr 5266  Ord word 6364  Oncon0 6365  ωcom 7855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-on 6369  df-lim 6370  df-om 7856

This theorem is referenced by:  omon  7867  limom  7871  ssnlim  7875  omsindsOLD  7877  peano5  7884  peano5OLD  7885  omsucelsucb  8458  nnarcl  8616  nnawordex  8637  oaabslem  8646  oaabs2  8648  omabslem  8649  onomeneqOLD  9229  ominf  9258  ominfOLD  9259  findcard3  9285  findcard3OLD  9286  nnsdomg  9302  nnsdomgOLD  9303  dffi3  9426  wofib  9540  alephgeom  10077  iscard3  10088  iunfictbso  10109  unctb  10200  ackbij2lem1  10214  ackbij1lem3  10217  ackbij1lem18  10232  ackbij2  10238  cflim2  10258  fin23lem26  10320  fin23lem23  10321  fin23lem27  10323  fin67  10390  alephexp1  10574  pwfseqlem3  10655  pwdjundom  10662  winainflem  10688  wunex2  10733  om2uzoi  13920  ltweuz  13926  fz1isolem  14422  1stcrestlem  22956  satfn  34346  hfuni  35156  hfninf  35158  finxpreclem4  36275  oaordnrex  42045  omnord1ex  42054  oenord1ex  42065  omabs2  42082  tfsconcat0b  42096  rn1st  43978