Theorem ordom 7921

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 7920	. 2 ⊢ Tr ω
2		omsson 7915	. 2 ⊢ ω ⊆ On
3		ordon 7823	. 2 ⊢ Ord On
4		trssord 6405	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1491	1 ⊢ Ord ω

This proof depends on syntax axioms:   ⊆ wss 3900  Tr wtr 5218  Ord word 6387  Oncon0 6388  ωcom 7911

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-tr 5219  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6391  df-on 6392  df-lim 6393  df-om 7912

This theorem is used by:  omon  7923  limom  7927  ssnlim  7931  peano5  7939  omsucelsucb  8506  nnarcl  8663  nnawordex  8684  oaabslem  8694  oaabs2  8696  omabslem  8697  ominf  9293  findcard3  9312  nnsdomg  9329  tfsnfin2  9390  dffi3  9460  wofib  9576  hfuniOLD  9962  alephgeom  10200  iscard3  10211  iunfictbso  10232  unctb  10321  ackbij2lem1  10335  ackbij1lem3  10338  ackbij1lem18  10353  ackbij2  10359  cflim2  10380  fin23lem26  10442  fin23lem23  10443  fin23lem27  10445  fin67  10512  alephexp1  10703  pwfseqlem3  10784  pwdjundom  10791  winainflem  10817  wunex2  10862  om2uzoi  14138  ltweuz  14144  fz1isolem  14647  1stcrestlem  23825  om2noseqoi  28746  oldfib  28820  z12bdaylem  28927  satfn  36328  hfninf  37150  bj-iomnnom  38448  finxpreclem4  38585  oaordnrex  44558  omnord1ex  44567  oenord1ex  44578  omabs2  44595  tfsconcat0b  44609  hfstructwe  46303  rn1st  46558