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

Theorem ordom 4667
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 4117 . . 3  |-  ( Tr 
om 
<-> 
A. y A. x
( ( y  e.  x  /\  x  e. 
om )  ->  y  e.  om ) )
2 onelon 4419 . . . . . . . 8  |-  ( ( x  e.  On  /\  y  e.  x )  ->  y  e.  On )
32expcom 424 . . . . . . 7  |-  ( y  e.  x  ->  (
x  e.  On  ->  y  e.  On ) )
4 limord 4453 . . . . . . . . . . . 12  |-  ( Lim  z  ->  Ord  z )
5 ordtr 4408 . . . . . . . . . . . 12  |-  ( Ord  z  ->  Tr  z
)
6 trel 4122 . . . . . . . . . . . 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 1609 . . . . . . 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 4661 . . . . . 6  |-  ( x  e.  om  <->  ( x  e.  On  /\  A. z
( Lim  z  ->  x  e.  z ) ) )
14 elom 4661 . . . . . 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 1535 . . 3  |-  A. x
( ( y  e.  x  /\  x  e. 
om )  ->  y  e.  om )
181, 17mpgbir 1539 . 2  |-  Tr  om
19 omsson 4662 . 2  |-  om  C_  On
20 ordon 4576 . 2  |-  Ord  On
21 trssord 4411 . 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 1529    e. wcel 1686    C_ wss 3154   Tr wtr 4115   Ord word 4393   Oncon0 4394   Lim wlim 4395   omcom 4658
This theorem is referenced by:  elnn  4668  omon  4669  limom  4673  ssnlim  4676  peano5  4681  nnarcl  6616  nnawordex  6637  oaabslem  6643  oaabs2  6645  omabslem  6646  onomeneq  7052  ominf  7077  findcard3  7102  nnsdomg  7118  dffi3  7186  wofib  7262  alephgeom  7711  iscard3  7722  iunfictbso  7743  unctb  7833  ackbij2lem1  7847  ackbij1lem3  7850  ackbij1lem18  7865  ackbij2  7871  cflim2  7891  fin23lem26  7953  fin23lem23  7954  fin23lem27  7956  fin67  8023  alephexp1  8203  pwfseqlem3  8284  pwcdandom  8291  winainflem  8317  wunex2  8362  om2uzoi  11020  ltweuz  11026  fz1isolem  11401  mreexexd  13552  1stcrestlem  17180  omsinds  24221  hfuni  24816  hfninf  24818
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216  ax-un 4514
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 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-tr 4116  df-eprel 4307  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659
  Copyright terms: Public domain W3C validator