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

Theorem ordom 6450
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

Proof of Theorem ordom
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dftr2 4397 . . 3
2 onelon 4747 . . . . . . . 8
32expcom 426 . . . . . . 7
4 limord 4781 . . . . . . . . . . . 12
5 ordtr 4736 . . . . . . . . . . . 12
6 trel 4402 . . . . . . . . . . . 12
74, 5, 63syl 19 . . . . . . . . . . 11
87exp3a 427 . . . . . . . . . 10
98com12 30 . . . . . . . . 9
109a2d 25 . . . . . . . 8
1110alimdv 1641 . . . . . . 7
123, 11anim12d 548 . . . . . 6
13 elom 6444 . . . . . 6
14 elom 6444 . . . . . 6
1512, 13, 143imtr4g 263 . . . . 5
1615imp 420 . . . 4
1716ax-gen 1562 . . 3
181, 17mpgbir 1566 . 2
19 omsson 6445 . 2
20 ordon 6359 . 2
21 trssord 4739 . 2
2218, 19, 20, 21mp3an 1287 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  A.wal 1556  e.wcel 1724  C_wss 3353  Trwtr 4395  Ordword 4721   con0 4722  Limwlim 4723   com 6441
This theorem is referenced by:  elnn  6451  omon  6452  limom  6456  ssnlim  6459  peano5  6464  nnarcl  6971  nnawordex  6992  oaabslem  6998  oaabs2  7000  omabslem  7001  onomeneq  7408  ominf  7433  findcard3  7462  nnsdomg  7478  dffi3  7548  wofib  7626  alephgeom  8077  iscard3  8088  iunfictbso  8109  unctb  8199  ackbij2lem1  8213  ackbij1lem3  8216  ackbij1lem18  8231  ackbij2  8237  cflim2  8257  fin23lem26  8319  fin23lem23  8320  fin23lem27  8322  fin67  8389  alephexp1  8568  pwfseqlem3  8649  pwcdandom  8656  winainflem  8682  wunex2  8727  om2uzoi  11570  ltweuz  11576  fz1isolem  12001  mreexexd  14364  1stcrestlem  18019  omsinds  26324  hfuni  26955  hfninf  26957
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-8 1726  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pr 4538  ax-un 6338
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3008  df-sbc 3213  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-pss 3369  df-nul 3661  df-if 3813  df-sn 3900  df-pr 3901  df-tp 3902  df-op 3903  df-uni 4102  df-br 4303  df-opab 4361  df-tr 4396  df-eprel 4635  df-po 4644  df-so 4645  df-fr 4682  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-om 6442
  Copyright terms: Public domain W3C validator