Theorem ordom 7887

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 7886	. 2 ⊢ Tr ω
2		omsson 7881	. 2 ⊢ ω ⊆ On
3		ordon 7791	. 2 ⊢ Ord On
4		trssord 6379	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1490	1 ⊢ Ord ω

This proof depends on syntax axioms:   ⊆ wss 3899  Tr wtr 5212  Ord word 6361  Oncon0 6362  ωcom 7877

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 2733  ax-sep 5249  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 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6365  df-on 6366  df-lim 6367  df-om 7878

This theorem is used by:  omon  7889  limom  7893  ssnlim  7897  peano5  7905  omsucelsucb  8468  nnarcl  8625  nnawordex  8646  oaabslem  8656  oaabs2  8658  omabslem  8659  ominf  9255  findcard3  9274  nnsdomg  9291  tfsnfin2  9352  dffi3  9423  wofib  9539  hfuniOLD  9925  alephgeom  10161  iscard3  10172  iunfictbso  10193  unctb  10282  ackbij2lem1  10296  ackbij1lem3  10299  ackbij1lem18  10314  ackbij2  10320  cflim2  10341  fin23lem26  10403  fin23lem23  10404  fin23lem27  10406  fin67  10473  alephexp1  10664  pwfseqlem3  10745  pwdjundom  10752  winainflem  10778  wunex2  10823  om2uzoi  14098  ltweuz  14104  fz1isolem  14606  1stcrestlem  23770  om2noseqoi  28689  oldfib  28763  z12bdaylem  28870  satfn  36120  hfninf  36935  bj-iomnnom  38180  finxpreclem4  38317  oaordnrex  44296  omnord1ex  44305  oenord1ex  44316  omabs2  44333  tfsconcat0b  44347  rn1st  46284