Theorem ordom 6715

Description: Omega 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 om

Proof of Theorem ordom

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dftr2 4520	. . 3 |- ( Tr om <-> A. y A. x ( ( y e. x /\ x e. om ) -> y e. om ) )
2		onelon 5467	. . . . . . . 8 |- ( ( x e. On /\ y e. x ) -> y e. On )
3	2	expcom 436	. . . . . . 7 |- ( y e. x -> ( x e. On -> y e. On ) )
4		limord 5501	. . . . . . . . . . . 12 |- ( Lim z -> Ord z )
5		ordtr 5456	. . . . . . . . . . . 12 |- ( Ord z -> Tr z )
6		trel 4525	. . . . . . . . . . . 12 |- ( Tr z -> ( ( y e. x /\ x e. z ) -> y e. z ) )
7	4, 5, 6	3syl 18	. . . . . . . . . . 11 |- ( Lim z -> ( ( y e. x /\ x e. z ) -> y e. z ) )
8	7	expd 437	. . . . . . . . . 10 |- ( Lim z -> ( y e. x -> ( x e. z -> y e. z ) ) )
9	8	com12 32	. . . . . . . . 9 |- ( y e. x -> ( Lim z -> ( x e. z -> y e. z ) ) )
10	9	a2d 29	. . . . . . . 8 |- ( y e. x -> ( ( Lim z -> x e. z ) -> ( Lim z -> y e. z ) ) )
11	10	alimdv 1757	. . . . . . 7 |- ( y e. x -> ( A. z ( Lim z -> x e. z ) -> A. z ( Lim z -> y e. z ) ) )
12	3, 11	anim12d 565	. . . . . 6 |- ( y e. x -> ( ( x e. On /\ A. z ( Lim z -> x e. z ) ) -> ( y e. On /\ A. z ( Lim z -> y e. z ) ) ) )
13		elom 6709	. . . . . 6 |- ( x e. om <-> ( x e. On /\ A. z ( Lim z -> x e. z ) ) )
14		elom 6709	. . . . . 6 |- ( y e. om <-> ( y e. On /\ A. z ( Lim z -> y e. z ) ) )
15	12, 13, 14	3imtr4g 273	. . . . 5 |- ( y e. x -> ( x e. om -> y e. om ) )
16	15	imp 430	. . . 4 |- ( ( y e. x /\ x e. om ) -> y e. om )
17	16	ax-gen 1663	. . 3 |- A. x ( ( y e. x /\ x e. om ) -> y e. om )
18	1, 17	mpgbir 1667	. 2 |- Tr om
19		omsson 6710	. 2 |- om C_ On
20		ordon 6623	. 2 |- Ord On
21		trssord 5459	. 2 |- ( ( Tr om /\ om C_ On /\ Ord On ) -> Ord om )
22	18, 19, 20, 21	mp3an 1360	1 |- Ord om

Syntax hints:   -> wi 4   /\ wa 370   A.wal 1435   e. wcel 1872   C_ wss 3436   Tr wtr 4518   Ord word 5441   Oncon0 5442   Lim wlim 5443   omcom 6706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660  ax-un 6597

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-tr 4519  df-eprel 4764  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-om 6707

This theorem is referenced by:  elnn  6716  omon  6717  limom  6721  ssnlim  6724  omsinds  6725  peano5  6730  nnarcl  7328  nnawordex  7349  oaabslem  7355  oaabs2  7357  omabslem  7358  onomeneq  7771  ominf  7793  findcard3  7823  nnsdomg  7839  dffi3  7954  wofib  8069  alephgeom  8520  iscard3  8531  iunfictbso  8552  unctb  8642  ackbij2lem1  8656  ackbij1lem3  8659  ackbij1lem18  8674  ackbij2  8680  cflim2  8700  fin23lem26  8762  fin23lem23  8763  fin23lem27  8765  fin67  8832  alephexp1  9011  pwfseqlem3  9092  pwcdandom  9099  winainflem  9125  wunex2  9170  om2uzoi  12175  ltweuz  12181  fz1isolem  12628  mreexexd  15553  1stcrestlem  20465  hfuni  30956  hfninf  30958  finxpreclem4  31750