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

Theorem ordom 4895
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 4338 . . 3
2 onelon 4647 . . . . . . . 8
32expcom 426 . . . . . . 7
4 limord 4681 . . . . . . . . . . . 12
5 ordtr 4636 . . . . . . . . . . . 12
6 trel 4343 . . . . . . . . . . . 12
74, 5, 63syl 19 . . . . . . . . . . 11
87exp3a 427 . . . . . . . . . 10
98com12 30 . . . . . . . . 9
109a2d 25 . . . . . . . 8
1110alimdv 1633 . . . . . . 7
123, 11anim12d 548 . . . . . 6
13 elom 4889 . . . . . 6
14 elom 4889 . . . . . 6
1512, 13, 143imtr4g 263 . . . . 5
1615imp 420 . . . 4
1716ax-gen 1556 . . 3
181, 17mpgbir 1560 . 2
19 omsson 4890 . 2
20 ordon 4804 . 2
21 trssord 4639 . 2
2218, 19, 20, 21mp3an 1280 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  A.wal 1550  e.wcel 1728  C_wss 3309  Trwtr 4336  Ordword 4621   con0 4622  Limwlim 4623   com 4886
This theorem is referenced by:  elnn  4896  omon  4897  limom  4901  ssnlim  4904  peano5  4909  nnarcl  6908  nnawordex  6929  oaabslem  6935  oaabs2  6937  omabslem  6938  onomeneq  7345  ominf  7370  findcard3  7399  nnsdomg  7415  dffi3  7485  wofib  7563  alephgeom  8014  iscard3  8025  iunfictbso  8046  unctb  8136  ackbij2lem1  8150  ackbij1lem3  8153  ackbij1lem18  8168  ackbij2  8174  cflim2  8194  fin23lem26  8256  fin23lem23  8257  fin23lem27  8259  fin67  8326  alephexp1  8505  pwfseqlem3  8586  pwcdandom  8593  winainflem  8619  wunex2  8664  om2uzoi  11346  ltweuz  11352  fz1isolem  11761  mreexexd  13924  1stcrestlem  17566  omsinds  25598  hfuni  26229  hfninf  26231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4364  ax-nul 4372  ax-pr 4442  ax-un 4742
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-sbc 3171  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-pss 3325  df-nul 3617  df-if 3766  df-sn 3847  df-pr 3848  df-tp 3849  df-op 3850  df-uni 4044  df-br 4244  df-opab 4302  df-tr 4337  df-eprel 4535  df-po 4544  df-so 4545  df-fr 4582  df-we 4584  df-ord 4625  df-on 4626  df-lim 4627  df-suc 4628  df-om 4887
  Copyright terms: Public domain W3C validator