Theorem ordom 6733

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 4515	. . 3 |- ( Tr om <-> A. y A. x ( ( y e. x /\ x e. om ) -> y e. om ) )
2		onelon 5471	. . . . . . . 8 |- ( ( x e. On /\ y e. x ) -> y e. On )
3	2	expcom 441	. . . . . . 7 |- ( y e. x -> ( x e. On -> y e. On ) )
4		limord 5505	. . . . . . . . . . . 12 |- ( Lim z -> Ord z )
5		ordtr 5460	. . . . . . . . . . . 12 |- ( Ord z -> Tr z )
6		trel 4520	. . . . . . . . . . . 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 442	. . . . . . . . . 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 1774	. . . . . . 7 |- ( y e. x -> ( A. z ( Lim z -> x e. z ) -> A. z ( Lim z -> y e. z ) ) )
12	3, 11	anim12d 570	. . . . . 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 6727	. . . . . 6 |- ( x e. om <-> ( x e. On /\ A. z ( Lim z -> x e. z ) ) )
14		elom 6727	. . . . . 6 |- ( y e. om <-> ( y e. On /\ A. z ( Lim z -> y e. z ) ) )
15	12, 13, 14	3imtr4g 278	. . . . 5 |- ( y e. x -> ( x e. om -> y e. om ) )
16	15	imp 435	. . . 4 |- ( ( y e. x /\ x e. om ) -> y e. om )
17	16	ax-gen 1680	. . 3 |- A. x ( ( y e. x /\ x e. om ) -> y e. om )
18	1, 17	mpgbir 1684	. 2 |- Tr om
19		omsson 6728	. 2 |- om C_ On
20		ordon 6641	. 2 |- Ord On
21		trssord 5463	. 2 |- ( ( Tr om /\ om C_ On /\ Ord On ) -> Ord om )
22	18, 19, 20, 21	mp3an 1373	1 |- Ord om

Syntax hints:   -> wi 4   /\ wa 375   A.wal 1453   e. wcel 1898   C_ wss 3416   Tr wtr 4513   Ord word 5445   Oncon0 5446   Lim wlim 5447   omcom 6724

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pr 4656  ax-un 6615

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-tr 4514  df-eprel 4767  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-om 6725

This theorem is referenced by:  elnn  6734  omon  6735  limom  6739  ssnlim  6742  omsinds  6743  peano5  6748  nnarcl  7348  nnawordex  7369  oaabslem  7375  oaabs2  7377  omabslem  7378  onomeneq  7793  ominf  7815  findcard3  7845  nnsdomg  7861  dffi3  7976  wofib  8091  alephgeom  8544  iscard3  8555  iunfictbso  8576  unctb  8666  ackbij2lem1  8680  ackbij1lem3  8683  ackbij1lem18  8698  ackbij2  8704  cflim2  8724  fin23lem26  8786  fin23lem23  8787  fin23lem27  8789  fin67  8856  alephexp1  9035  pwfseqlem3  9116  pwcdandom  9123  winainflem  9149  wunex2  9194  om2uzoi  12207  ltweuz  12213  fz1isolem  12663  mreexexd  15609  1stcrestlem  20522  hfuni  31001  hfninf  31003  finxpreclem4  31832