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

Theorem ordom 6626
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 4475 . . 3  |-  ( Tr 
om 
<-> 
A. y A. x
( ( y  e.  x  /\  x  e. 
om )  ->  y  e.  om ) )
2 onelon 4830 . . . . . . . 8  |-  ( ( x  e.  On  /\  y  e.  x )  ->  y  e.  On )
32expcom 433 . . . . . . 7  |-  ( y  e.  x  ->  (
x  e.  On  ->  y  e.  On ) )
4 limord 4864 . . . . . . . . . . . 12  |-  ( Lim  z  ->  Ord  z )
5 ordtr 4819 . . . . . . . . . . . 12  |-  ( Ord  z  ->  Tr  z
)
6 trel 4480 . . . . . . . . . . . 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 ) )
87expd 434 . . . . . . . . . 10  |-  ( Lim  z  ->  ( y  e.  x  ->  ( x  e.  z  ->  y  e.  z ) ) )
98com12 31 . . . . . . . . 9  |-  ( y  e.  x  ->  ( Lim  z  ->  ( x  e.  z  ->  y  e.  z ) ) )
109a2d 26 . . . . . . . 8  |-  ( y  e.  x  ->  (
( Lim  z  ->  x  e.  z )  -> 
( Lim  z  ->  y  e.  z ) ) )
1110alimdv 1724 . . . . . . 7  |-  ( y  e.  x  ->  ( A. z ( Lim  z  ->  x  e.  z )  ->  A. z ( Lim  z  ->  y  e.  z ) ) )
123, 11anim12d 561 . . . . . 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 6620 . . . . . 6  |-  ( x  e.  om  <->  ( x  e.  On  /\  A. z
( Lim  z  ->  x  e.  z ) ) )
14 elom 6620 . . . . . 6  |-  ( y  e.  om  <->  ( y  e.  On  /\  A. z
( Lim  z  ->  y  e.  z ) ) )
1512, 13, 143imtr4g 270 . . . . 5  |-  ( y  e.  x  ->  (
x  e.  om  ->  y  e.  om ) )
1615imp 427 . . . 4  |-  ( ( y  e.  x  /\  x  e.  om )  ->  y  e.  om )
1716ax-gen 1633 . . 3  |-  A. x
( ( y  e.  x  /\  x  e. 
om )  ->  y  e.  om )
181, 17mpgbir 1637 . 2  |-  Tr  om
19 omsson 6621 . 2  |-  om  C_  On
20 ordon 6535 . 2  |-  Ord  On
21 trssord 4822 . 2  |-  ( ( Tr  om  /\  om  C_  On  /\  Ord  On )  ->  Ord  om )
2218, 19, 20, 21mp3an 1322 1  |-  Ord  om
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367   A.wal 1397    e. wcel 1836    C_ wss 3402   Tr wtr 4473   Ord word 4804   Oncon0 4805   Lim wlim 4806   omcom 6617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pr 4614  ax-un 6509
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-tr 4474  df-eprel 4718  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-om 6618
This theorem is referenced by:  elnn  6627  omon  6628  limom  6632  ssnlim  6635  peano5  6640  nnarcl  7201  nnawordex  7222  oaabslem  7228  oaabs2  7230  omabslem  7231  onomeneq  7644  ominf  7666  findcard3  7696  nnsdomg  7712  dffi3  7824  wofib  7903  alephgeom  8394  iscard3  8405  iunfictbso  8426  unctb  8516  ackbij2lem1  8530  ackbij1lem3  8533  ackbij1lem18  8548  ackbij2  8554  cflim2  8574  fin23lem26  8636  fin23lem23  8637  fin23lem27  8639  fin67  8706  alephexp1  8885  pwfseqlem3  8967  pwcdandom  8974  winainflem  9000  wunex2  9045  om2uzoi  11988  ltweuz  11994  fz1isolem  12433  mreexexd  15074  1stcrestlem  20057  omsinds  29500  hfuni  30030  hfninf  30032
  Copyright terms: Public domain W3C validator