Theorem ordom 7873

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 7872	. 2 ⊢ Tr ω
2		omsson 7867	. 2 ⊢ ω ⊆ On
3		ordon 7777	. 2 ⊢ Ord On
4		trssord 6374	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1490	1 ⊢ Ord ω

This proof depends on syntax axioms:   ⊆ wss 3899  Tr wtr 5212  Ord word 6356  Oncon0 6357  ωcom 7863

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6360  df-on 6361  df-lim 6362  df-om 7864

This theorem is used by:  omon  7875  limom  7879  ssnlim  7883  peano5  7891  omsucelsucb  8448  nnarcl  8605  nnawordex  8626  oaabslem  8636  oaabs2  8638  omabslem  8639  ominf  9235  findcard3  9254  nnsdomg  9270  tfsnfin2  9331  dffi3  9402  wofib  9518  alephgeom  10086  iscard3  10097  iunfictbso  10118  unctb  10207  ackbij2lem1  10221  ackbij1lem3  10224  ackbij1lem18  10239  ackbij2  10245  cflim2  10266  fin23lem26  10328  fin23lem23  10329  fin23lem27  10331  fin67  10398  alephexp1  10589  pwfseqlem3  10670  pwdjundom  10677  winainflem  10703  wunex2  10748  om2uzoi  14020  ltweuz  14026  fz1isolem  14527  1stcrestlem  23678  om2noseqoi  28569  oldfib  28643  z12bdaylem  28750  satfn  35935  hfuni  36765  hfninf  36767  bj-iomnnom  38012  finxpreclem4  38149  oaordnrex  44137  omnord1ex  44146  oenord1ex  44157  omabs2  44174  tfsconcat0b  44188  rn1st  46103