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

Theorem ordom 4817
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 4268 . . 3  |-  ( Tr 
om 
<-> 
A. y A. x
( ( y  e.  x  /\  x  e. 
om )  ->  y  e.  om ) )
2 onelon 4570 . . . . . . . 8  |-  ( ( x  e.  On  /\  y  e.  x )  ->  y  e.  On )
32expcom 425 . . . . . . 7  |-  ( y  e.  x  ->  (
x  e.  On  ->  y  e.  On ) )
4 limord 4604 . . . . . . . . . . . 12  |-  ( Lim  z  ->  Ord  z )
5 ordtr 4559 . . . . . . . . . . . 12  |-  ( Ord  z  ->  Tr  z
)
6 trel 4273 . . . . . . . . . . . 12  |-  ( Tr  z  ->  ( (
y  e.  x  /\  x  e.  z )  ->  y  e.  z ) )
74, 5, 63syl 19 . . . . . . . . . . 11  |-  ( Lim  z  ->  ( (
y  e.  x  /\  x  e.  z )  ->  y  e.  z ) )
87exp3a 426 . . . . . . . . . 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 24 . . . . . . . 8  |-  ( y  e.  x  ->  (
( Lim  z  ->  x  e.  z )  -> 
( Lim  z  ->  y  e.  z ) ) )
1110alimdv 1628 . . . . . . 7  |-  ( y  e.  x  ->  ( A. z ( Lim  z  ->  x  e.  z )  ->  A. z ( Lim  z  ->  y  e.  z ) ) )
123, 11anim12d 547 . . . . . 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 4811 . . . . . 6  |-  ( x  e.  om  <->  ( x  e.  On  /\  A. z
( Lim  z  ->  x  e.  z ) ) )
14 elom 4811 . . . . . 6  |-  ( y  e.  om  <->  ( y  e.  On  /\  A. z
( Lim  z  ->  y  e.  z ) ) )
1512, 13, 143imtr4g 262 . . . . 5  |-  ( y  e.  x  ->  (
x  e.  om  ->  y  e.  om ) )
1615imp 419 . . . 4  |-  ( ( y  e.  x  /\  x  e.  om )  ->  y  e.  om )
1716ax-gen 1552 . . 3  |-  A. x
( ( y  e.  x  /\  x  e. 
om )  ->  y  e.  om )
181, 17mpgbir 1556 . 2  |-  Tr  om
19 omsson 4812 . 2  |-  om  C_  On
20 ordon 4726 . 2  |-  Ord  On
21 trssord 4562 . 2  |-  ( ( Tr  om  /\  om  C_  On  /\  Ord  On )  ->  Ord  om )
2218, 19, 20, 21mp3an 1279 1  |-  Ord  om
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1546    e. wcel 1721    C_ wss 3284   Tr wtr 4266   Ord word 4544   Oncon0 4545   Lim wlim 4546   omcom 4808
This theorem is referenced by:  elnn  4818  omon  4819  limom  4823  ssnlim  4826  peano5  4831  nnarcl  6822  nnawordex  6843  oaabslem  6849  oaabs2  6851  omabslem  6852  onomeneq  7259  ominf  7284  findcard3  7313  nnsdomg  7329  dffi3  7398  wofib  7474  alephgeom  7923  iscard3  7934  iunfictbso  7955  unctb  8045  ackbij2lem1  8059  ackbij1lem3  8062  ackbij1lem18  8077  ackbij2  8083  cflim2  8103  fin23lem26  8165  fin23lem23  8166  fin23lem27  8168  fin67  8235  alephexp1  8414  pwfseqlem3  8495  pwcdandom  8502  winainflem  8528  wunex2  8573  om2uzoi  11254  ltweuz  11260  fz1isolem  11669  mreexexd  13832  1stcrestlem  17472  omsinds  25437  hfuni  26033  hfninf  26035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367  ax-un 4664
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-pss 3300  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-tp 3786  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-tr 4267  df-eprel 4458  df-po 4467  df-so 4468  df-fr 4505  df-we 4507  df-ord 4548  df-on 4549  df-lim 4550  df-suc 4551  df-om 4809
  Copyright terms: Public domain W3C validator