Theorem ordom 7878

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

This proof depends on syntax axioms:   ⊆ wss 3906  Tr wtr 5220  Ord word 6363  Oncon0 6364  ωcom 7868

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368  df-lim 6369  df-om 7869

This theorem is used by:  omon  7880  limom  7884  ssnlim  7888  peano5  7896  omsucelsucb  8451  nnarcl  8608  nnawordex  8629  oaabslem  8639  oaabs2  8641  omabslem  8642  ominf  9231  findcard3  9250  nnsdomg  9266  tfsnfin2  9327  dffi3  9398  wofib  9514  alephgeom  10082  iscard3  10093  iunfictbso  10114  unctb  10203  ackbij2lem1  10217  ackbij1lem3  10220  ackbij1lem18  10235  ackbij2  10241  cflim2  10262  fin23lem26  10324  fin23lem23  10325  fin23lem27  10327  fin67  10394  alephexp1  10579  pwfseqlem3  10660  pwdjundom  10667  winainflem  10693  wunex2  10738  om2uzoi  14009  ltweuz  14015  fz1isolem  14516  1stcrestlem  23659  om2noseqoi  28547  oldfib  28621  z12bdaylem  28728  satfn  35884  hfuni  36713  hfninf  36715  bj-iomnnom  37960  finxpreclem4  38097  oaordnrex  44080  omnord1ex  44089  oenord1ex  44100  omabs2  44117  tfsconcat0b  44131  rn1st  46046