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

Theorem ordom 4747
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 4196 . . 3  |-  ( Tr 
om 
<-> 
A. y A. x
( ( y  e.  x  /\  x  e. 
om )  ->  y  e.  om ) )
2 onelon 4499 . . . . . . . 8  |-  ( ( x  e.  On  /\  y  e.  x )  ->  y  e.  On )
32expcom 424 . . . . . . 7  |-  ( y  e.  x  ->  (
x  e.  On  ->  y  e.  On ) )
4 limord 4533 . . . . . . . . . . . 12  |-  ( Lim  z  ->  Ord  z )
5 ordtr 4488 . . . . . . . . . . . 12  |-  ( Ord  z  ->  Tr  z
)
6 trel 4201 . . . . . . . . . . . 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 1621 . . . . . . 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 4741 . . . . . 6  |-  ( x  e.  om  <->  ( x  e.  On  /\  A. z
( Lim  z  ->  x  e.  z ) ) )
14 elom 4741 . . . . . 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 1546 . . 3  |-  A. x
( ( y  e.  x  /\  x  e. 
om )  ->  y  e.  om )
181, 17mpgbir 1550 . 2  |-  Tr  om
19 omsson 4742 . 2  |-  om  C_  On
20 ordon 4656 . 2  |-  Ord  On
21 trssord 4491 . 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 1540    e. wcel 1710    C_ wss 3228   Tr wtr 4194   Ord word 4473   Oncon0 4474   Lim wlim 4475   omcom 4738
This theorem is referenced by:  elnn  4748  omon  4749  limom  4753  ssnlim  4756  peano5  4761  nnarcl  6701  nnawordex  6722  oaabslem  6728  oaabs2  6730  omabslem  6731  onomeneq  7138  ominf  7163  findcard3  7190  nnsdomg  7206  dffi3  7274  wofib  7350  alephgeom  7799  iscard3  7810  iunfictbso  7831  unctb  7921  ackbij2lem1  7935  ackbij1lem3  7938  ackbij1lem18  7953  ackbij2  7959  cflim2  7979  fin23lem26  8041  fin23lem23  8042  fin23lem27  8044  fin67  8111  alephexp1  8291  pwfseqlem3  8372  pwcdandom  8379  winainflem  8405  wunex2  8450  om2uzoi  11110  ltweuz  11116  fz1isolem  11495  mreexexd  13649  1stcrestlem  17284  omsinds  24777  hfuni  25373  hfninf  25375
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pr 4295  ax-un 4594
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-tr 4195  df-eprel 4387  df-po 4396  df-so 4397  df-fr 4434  df-we 4436  df-ord 4477  df-on 4478  df-lim 4479  df-suc 4480  df-om 4739
  Copyright terms: Public domain W3C validator