Theorem ordom 7852

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 7851	. 2 ⊢ Tr ω
2		omsson 7846	. 2 ⊢ ω ⊆ On
3		ordon 7753	. 2 ⊢ Ord On
4		trssord 6349	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1463	1 ⊢ Ord ω

Syntax hints:   ⊆ wss 3914  Tr wtr 5214  Ord word 6331  Oncon0 6332  ωcom 7842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336  df-lim 6337  df-om 7843

This theorem is referenced by:  omon  7854  limom  7858  ssnlim  7862  peano5  7869  omsucelsucb  8426  nnarcl  8580  nnawordex  8601  oaabslem  8611  oaabs2  8613  omabslem  8614  ominf  9205  ominfOLD  9206  findcard3  9229  findcard3OLD  9230  nnsdomg  9246  nnsdomgOLD  9247  dffi3  9382  wofib  9498  alephgeom  10035  iscard3  10046  iunfictbso  10067  unctb  10157  ackbij2lem1  10171  ackbij1lem3  10174  ackbij1lem18  10189  ackbij2  10195  cflim2  10216  fin23lem26  10278  fin23lem23  10279  fin23lem27  10281  fin67  10348  alephexp1  10532  pwfseqlem3  10613  pwdjundom  10620  winainflem  10646  wunex2  10691  om2uzoi  13920  ltweuz  13926  fz1isolem  14426  1stcrestlem  23339  om2noseqoi  28197  satfn  35342  hfuni  36172  hfninf  36174  finxpreclem4  37382  oaordnrex  43284  omnord1ex  43293  oenord1ex  43304  omabs2  43321  tfsconcat0b  43335  rn1st  45267