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

Theorem ordom 4602
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
StepHypRef Expression
1 dftr2 4055 . . 3  |-  ( Tr 
om 
<-> 
A. y A. x
( ( y  e.  x  /\  x  e. 
om )  ->  y  e.  om ) )
2 onelon 4354 . . . . . . . 8  |-  ( ( x  e.  On  /\  y  e.  x )  ->  y  e.  On )
32expcom 426 . . . . . . 7  |-  ( y  e.  x  ->  (
x  e.  On  ->  y  e.  On ) )
4 limord 4388 . . . . . . . . . . . 12  |-  ( Lim  z  ->  Ord  z )
5 ordtr 4343 . . . . . . . . . . . 12  |-  ( Ord  z  ->  Tr  z
)
6 trel 4060 . . . . . . . . . . . 12  |-  ( Tr  z  ->  ( (
y  e.  x  /\  x  e.  z )  ->  y  e.  z ) )
74, 5, 63syl 20 . . . . . . . . . . 11  |-  ( Lim  z  ->  ( (
y  e.  x  /\  x  e.  z )  ->  y  e.  z ) )
87exp3a 427 . . . . . . . . . 10  |-  ( Lim  z  ->  ( y  e.  x  ->  ( x  e.  z  ->  y  e.  z ) ) )
98com12 29 . . . . . . . . 9  |-  ( y  e.  x  ->  ( Lim  z  ->  ( x  e.  z  ->  y  e.  z ) ) )
109a2d 25 . . . . . . . 8  |-  ( y  e.  x  ->  (
( Lim  z  ->  x  e.  z )  -> 
( Lim  z  ->  y  e.  z ) ) )
1110alimdv 2018 . . . . . . 7  |-  ( y  e.  x  ->  ( A. z ( Lim  z  ->  x  e.  z )  ->  A. z ( Lim  z  ->  y  e.  z ) ) )
123, 11anim12d 548 . . . . . 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 4596 . . . . . 6  |-  ( x  e.  om  <->  ( x  e.  On  /\  A. z
( Lim  z  ->  x  e.  z ) ) )
14 elom 4596 . . . . . 6  |-  ( y  e.  om  <->  ( y  e.  On  /\  A. z
( Lim  z  ->  y  e.  z ) ) )
1512, 13, 143imtr4g 263 . . . . 5  |-  ( y  e.  x  ->  (
x  e.  om  ->  y  e.  om ) )
1615imp 420 . . . 4  |-  ( ( y  e.  x  /\  x  e.  om )  ->  y  e.  om )
1716ax-gen 1536 . . 3  |-  A. x
( ( y  e.  x  /\  x  e. 
om )  ->  y  e.  om )
181, 17mpgbir 1544 . 2  |-  Tr  om
19 omsson 4597 . 2  |-  om  C_  On
20 ordon 4511 . 2  |-  Ord  On
21 trssord 4346 . 2  |-  ( ( Tr  om  /\  om  C_  On  /\  Ord  On )  ->  Ord  om )
2218, 19, 20, 21mp3an 1282 1  |-  Ord  om
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360   A.wal 1532    e. wcel 1621    C_ wss 3094   Tr wtr 4053   Ord word 4328   Oncon0 4329   Lim wlim 4330   omcom 4593
This theorem is referenced by:  elnn  4603  omon  4604  limom  4608  ssnlim  4611  peano5  4616  nnarcl  6547  nnawordex  6568  oaabslem  6574  oaabs2  6576  omabslem  6577  onomeneq  6983  ominf  7008  findcard3  7033  nnsdomg  7049  dffi3  7117  wofib  7193  alephgeom  7642  iscard3  7653  iunfictbso  7674  unctb  7764  ackbij2lem1  7778  ackbij1lem3  7781  ackbij1lem18  7796  ackbij2  7802  cflim2  7822  fin23lem26  7884  fin23lem23  7885  fin23lem27  7887  fin67  7954  alephexp1  8134  pwfseqlem3  8215  pwcdandom  8222  winainflem  8248  wunex2  8293  om2uzoi  10949  ltweuz  10955  fz1isolem  11329  mreexexd  13477  1stcrestlem  17105  omsinds  23553  hfuni  24154  hfninf  24156
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pr 4152  ax-un 4449
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-rab 2523  df-v 2742  df-sbc 2936  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-pss 3110  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-tp 3589  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-tr 4054  df-eprel 4242  df-po 4251  df-so 4252  df-fr 4289  df-we 4291  df-ord 4332  df-on 4333  df-lim 4334  df-suc 4335  df-om 4594
  Copyright terms: Public domain W3C validator