Theorem ordom 6626

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 4475	. . 3 |- ( Tr om <-> A. y A. x ( ( y e. x /\ x e. om ) -> y e. om ) )
2		onelon 4830	. . . . . . . 8 |- ( ( x e. On /\ y e. x ) -> y e. On )
3	2	expcom 433	. . . . . . 7 |- ( y e. x -> ( x e. On -> y e. On ) )
4		limord 4864	. . . . . . . . . . . 12 |- ( Lim z -> Ord z )
5		ordtr 4819	. . . . . . . . . . . 12 |- ( Ord z -> Tr z )
6		trel 4480	. . . . . . . . . . . 12 |- ( Tr z -> ( ( y e. x /\ x e. z ) -> y e. z ) )
7	4, 5, 6	3syl 20	. . . . . . . . . . 11 |- ( Lim z -> ( ( y e. x /\ x e. z ) -> y e. z ) )
8	7	expd 434	. . . . . . . . . 10 |- ( Lim z -> ( y e. x -> ( x e. z -> y e. z ) ) )
9	8	com12 31	. . . . . . . . 9 |- ( y e. x -> ( Lim z -> ( x e. z -> y e. z ) ) )
10	9	a2d 26	. . . . . . . 8 |- ( y e. x -> ( ( Lim z -> x e. z ) -> ( Lim z -> y e. z ) ) )
11	10	alimdv 1724	. . . . . . 7 |- ( y e. x -> ( A. z ( Lim z -> x e. z ) -> A. z ( Lim z -> y e. z ) ) )
12	3, 11	anim12d 561	. . . . . 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 6620	. . . . . 6 |- ( x e. om <-> ( x e. On /\ A. z ( Lim z -> x e. z ) ) )
14		elom 6620	. . . . . 6 |- ( y e. om <-> ( y e. On /\ A. z ( Lim z -> y e. z ) ) )
15	12, 13, 14	3imtr4g 270	. . . . 5 |- ( y e. x -> ( x e. om -> y e. om ) )
16	15	imp 427	. . . 4 |- ( ( y e. x /\ x e. om ) -> y e. om )
17	16	ax-gen 1633	. . 3 |- A. x ( ( y e. x /\ x e. om ) -> y e. om )
18	1, 17	mpgbir 1637	. 2 |- Tr om
19		omsson 6621	. 2 |- om C_ On
20		ordon 6535	. 2 |- Ord On
21		trssord 4822	. 2 |- ( ( Tr om /\ om C_ On /\ Ord On ) -> Ord om )
22	18, 19, 20, 21	mp3an 1322	1 |- Ord om

Syntax hints:   -> wi 4   /\ wa 367   A.wal 1397   e. wcel 1836   C_ wss 3402   Tr wtr 4473   Ord word 4804   Oncon0 4805   Lim wlim 4806   omcom 6617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pr 4614  ax-un 6509

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-tr 4474  df-eprel 4718  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-om 6618

This theorem is referenced by:  elnn  6627  omon  6628  limom  6632  ssnlim  6635  peano5  6640  nnarcl  7201  nnawordex  7222  oaabslem  7228  oaabs2  7230  omabslem  7231  onomeneq  7644  ominf  7666  findcard3  7696  nnsdomg  7712  dffi3  7824  wofib  7903  alephgeom  8394  iscard3  8405  iunfictbso  8426  unctb  8516  ackbij2lem1  8530  ackbij1lem3  8533  ackbij1lem18  8548  ackbij2  8554  cflim2  8574  fin23lem26  8636  fin23lem23  8637  fin23lem27  8639  fin67  8706  alephexp1  8885  pwfseqlem3  8967  pwcdandom  8974  winainflem  9000  wunex2  9045  om2uzoi  11988  ltweuz  11994  fz1isolem  12433  mreexexd  15074  1stcrestlem  20057  omsinds  29500  hfuni  30030  hfninf  30032