Theorem ordom 7868

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

Syntax hints:   ⊆ wss 3905  Tr wtr 5218  Ord word 6359  Oncon0 6360  ωcom 7858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-tr 5219  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-ord 6363  df-on 6364  df-lim 6365  df-om 7859

This theorem is referenced by:  omon  7870  limom  7874  ssnlim  7878  peano5  7886  omsucelsucb  8441  nnarcl  8598  nnawordex  8619  oaabslem  8629  oaabs2  8631  omabslem  8632  ominf  9220  findcard3  9239  nnsdomg  9255  tfsnfin2  9316  dffi3  9387  wofib  9503  alephgeom  10062  iscard3  10073  iunfictbso  10094  unctb  10183  ackbij2lem1  10197  ackbij1lem3  10200  ackbij1lem18  10215  ackbij2  10221  cflim2  10242  fin23lem26  10304  fin23lem23  10305  fin23lem27  10307  fin67  10374  alephexp1  10559  pwfseqlem3  10640  pwdjundom  10647  winainflem  10673  wunex2  10718  om2uzoi  13987  ltweuz  13993  fz1isolem  14494  1stcrestlem  23609  om2noseqoi  28496  oldfib  28570  z12bdaylem  28677  satfn  35847  hfuni  36676  hfninf  36678  bj-iomnnom  37903  finxpreclem4  38040  oaordnrex  44022  omnord1ex  44031  oenord1ex  44042  omabs2  44059  tfsconcat0b  44073  rn1st  45988