Theorem ordom 7876

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 7875	. 2 ⊢ Tr ω
2		omsson 7870	. 2 ⊢ ω ⊆ On
3		ordon 7780	. 2 ⊢ Ord On
4		trssord 6378	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1490	1 ⊢ Ord ω

This proof depends on syntax axioms:   ⊆ wss 3902  Tr wtr 5216  Ord word 6360  Oncon0 6361  ωcom 7866

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 2734  ax-sep 5255  ax-pr 5402

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-tr 5217  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365  df-lim 6366  df-om 7867

This theorem is used by:  omon  7878  limom  7882  ssnlim  7886  peano5  7894  omsucelsucb  8451  nnarcl  8608  nnawordex  8629  oaabslem  8639  oaabs2  8641  omabslem  8642  ominf  9238  findcard3  9257  nnsdomg  9273  tfsnfin2  9334  dffi3  9405  wofib  9521  alephgeom  10089  iscard3  10100  iunfictbso  10121  unctb  10210  ackbij2lem1  10224  ackbij1lem3  10227  ackbij1lem18  10242  ackbij2  10248  cflim2  10269  fin23lem26  10331  fin23lem23  10332  fin23lem27  10334  fin67  10401  alephexp1  10592  pwfseqlem3  10673  pwdjundom  10680  winainflem  10706  wunex2  10751  om2uzoi  14023  ltweuz  14029  fz1isolem  14530  1stcrestlem  23683  om2noseqoi  28576  oldfib  28650  z12bdaylem  28757  satfn  35942  hfuni  36772  hfninf  36774  bj-iomnnom  38019  finxpreclem4  38156  oaordnrex  44144  omnord1ex  44153  oenord1ex  44164  omabs2  44181  tfsconcat0b  44195  rn1st  46110