MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordom Unicode version

Theorem ordom 4664
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.
StepHypRef Expression
1 dftr2 4116 . . 3  |-  ( Tr 
om 
<-> 
A. y A. x
( ( y  e.  x  /\  x  e. 
om )  ->  y  e.  om ) )
2 onelon 4416 . . . . . . . 8  |-  ( ( x  e.  On  /\  y  e.  x )  ->  y  e.  On )
32expcom 424 . . . . . . 7  |-  ( y  e.  x  ->  (
x  e.  On  ->  y  e.  On ) )
4 limord 4450 . . . . . . . . . . . 12  |-  ( Lim  z  ->  Ord  z )
5 ordtr 4405 . . . . . . . . . . . 12  |-  ( Ord  z  ->  Tr  z
)
6 trel 4121 . . . . . . . . . . . 12  |-  ( Tr  z  ->  ( (
y  e.  x  /\  x  e.  z )  ->  y  e.  z ) )
74, 5, 63syl 18 . . . . . . . . . . 11  |-  ( Lim  z  ->  ( (
y  e.  x  /\  x  e.  z )  ->  y  e.  z ) )
87exp3a 425 . . . . . . . . . 10  |-  ( Lim  z  ->  ( y  e.  x  ->  ( x  e.  z  ->  y  e.  z ) ) )
98com12 27 . . . . . . . . 9  |-  ( y  e.  x  ->  ( Lim  z  ->  ( x  e.  z  ->  y  e.  z ) ) )
109a2d 23 . . . . . . . 8  |-  ( y  e.  x  ->  (
( Lim  z  ->  x  e.  z )  -> 
( Lim  z  ->  y  e.  z ) ) )
1110alimdv 1607 . . . . . . 7  |-  ( y  e.  x  ->  ( A. z ( Lim  z  ->  x  e.  z )  ->  A. z ( Lim  z  ->  y  e.  z ) ) )
123, 11anim12d 546 . . . . . 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 4658 . . . . . 6  |-  ( x  e.  om  <->  ( x  e.  On  /\  A. z
( Lim  z  ->  x  e.  z ) ) )
14 elom 4658 . . . . . 6  |-  ( y  e.  om  <->  ( y  e.  On  /\  A. z
( Lim  z  ->  y  e.  z ) ) )
1512, 13, 143imtr4g 261 . . . . 5  |-  ( y  e.  x  ->  (
x  e.  om  ->  y  e.  om ) )
1615imp 418 . . . 4  |-  ( ( y  e.  x  /\  x  e.  om )  ->  y  e.  om )
1716ax-gen 1533 . . 3  |-  A. x
( ( y  e.  x  /\  x  e. 
om )  ->  y  e.  om )
181, 17mpgbir 1537 . 2  |-  Tr  om
19 omsson 4659 . 2  |-  om  C_  On
20 ordon 4573 . 2  |-  Ord  On
21 trssord 4408 . 2  |-  ( ( Tr  om  /\  om  C_  On  /\  Ord  On )  ->  Ord  om )
2218, 19, 20, 21mp3an 1277 1  |-  Ord  om
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1527    e. wcel 1685    C_ wss 3153   Tr wtr 4114   Ord word 4390   Oncon0 4391   Lim wlim 4392   omcom 4655
This theorem is referenced by:  elnn  4665  omon  4666  limom  4670  ssnlim  4673  peano5  4678  nnarcl  6610  nnawordex  6631  oaabslem  6637  oaabs2  6639  omabslem  6640  onomeneq  7046  ominf  7071  findcard3  7096  nnsdomg  7112  dffi3  7180  wofib  7256  alephgeom  7705  iscard3  7716  iunfictbso  7737  unctb  7827  ackbij2lem1  7841  ackbij1lem3  7844  ackbij1lem18  7859  ackbij2  7865  cflim2  7885  fin23lem26  7947  fin23lem23  7948  fin23lem27  7950  fin67  8017  alephexp1  8197  pwfseqlem3  8278  pwcdandom  8285  winainflem  8311  wunex2  8356  om2uzoi  11014  ltweuz  11020  fz1isolem  11395  mreexexd  13546  1stcrestlem  17174  omsinds  23623  hfuni  24224  hfninf  24226
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-tr 4115  df-eprel 4304  df-po 4313  df-so 4314  df-fr 4351  df-we 4353  df-ord 4394  df-on 4395  df-lim 4396  df-suc 4397  df-om 4656
  Copyright terms: Public domain W3C validator