Theorem ordom 7716

Description: The class of finite ordinals ω is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43. (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 7715	. 2 ⊢ Tr ω
2		omsson 7710	. 2 ⊢ ω ⊆ On
3		ordon 7621	. 2 ⊢ Ord On
4		trssord 6282	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
5	1, 2, 3, 4	mp3an 1460	1 ⊢ Ord ω

Syntax hints:   ⊆ wss 3892  Tr wtr 5196  Ord word 6264  Oncon0 6265  ωcom 7706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-11 2158  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ne 2946  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-tr 5197  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-ord 6268  df-on 6269  df-lim 6270  df-om 7707

This theorem is referenced by:  omon  7718  limom  7722  ssnlim  7726  omsindsOLD  7728  peano5  7734  peano5OLD  7735  omsucelsucb  8280  nnarcl  8432  nnawordex  8453  oaabslem  8460  oaabs2  8462  omabslem  8463  onomeneq  8992  ominf  9013  findcard3  9035  nnsdomg  9051  dffi3  9168  wofib  9282  alephgeom  9839  iscard3  9850  iunfictbso  9871  unctb  9962  ackbij2lem1  9976  ackbij1lem3  9979  ackbij1lem18  9994  ackbij2  10000  cflim2  10020  fin23lem26  10082  fin23lem23  10083  fin23lem27  10085  fin67  10152  alephexp1  10336  pwfseqlem3  10417  pwdjundom  10424  winainflem  10450  wunex2  10495  om2uzoi  13673  ltweuz  13679  fz1isolem  14173  1stcrestlem  22601  satfn  33313  hfuni  34482  hfninf  34484  finxpreclem4  35561