Theorem ordom 7891

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 7890	. 2 ⊢ Tr ω
2		omsson 7885	. 2 ⊢ ω ⊆ On
3		ordon 7795	. 2 ⊢ Ord On
4		trssord 6382	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1490	1 ⊢ Ord ω

This proof depends on syntax axioms:   ⊆ wss 3896  Tr wtr 5211  Ord word 6364  Oncon0 6365  ωcom 7881

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  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-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6368  df-on 6369  df-lim 6370  df-om 7882

This theorem is used by:  omon  7893  limom  7897  ssnlim  7901  peano5  7909  omsucelsucb  8476  nnarcl  8633  nnawordex  8654  oaabslem  8664  oaabs2  8666  omabslem  8667  ominf  9263  findcard3  9282  nnsdomg  9299  tfsnfin2  9360  dffi3  9430  wofib  9546  hfuniOLD  9932  alephgeom  10168  iscard3  10179  iunfictbso  10200  unctb  10289  ackbij2lem1  10303  ackbij1lem3  10306  ackbij1lem18  10321  ackbij2  10327  cflim2  10348  fin23lem26  10410  fin23lem23  10411  fin23lem27  10413  fin67  10480  alephexp1  10671  pwfseqlem3  10752  pwdjundom  10759  winainflem  10785  wunex2  10830  om2uzoi  14105  ltweuz  14111  fz1isolem  14613  1stcrestlem  23779  om2noseqoi  28698  oldfib  28772  z12bdaylem  28879  satfn  36238  hfninf  37059  bj-iomnnom  38317  finxpreclem4  38454  oaordnrex  44434  omnord1ex  44443  oenord1ex  44454  omabs2  44471  tfsconcat0b  44485  rn1st  46421