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

Theorem ordom 6495
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 4413 . . 3
2 onelon 4765 . . . . . . . 8
32expcom 426 . . . . . . 7
4 limord 4799 . . . . . . . . . . . 12
5 ordtr 4754 . . . . . . . . . . . 12
6 trel 4418 . . . . . . . . . . . 12
74, 5, 63syl 19 . . . . . . . . . . 11
87exp3a 427 . . . . . . . . . 10
98com12 30 . . . . . . . . 9
109a2d 25 . . . . . . . 8
1110alimdv 1649 . . . . . . 7
123, 11anim12d 548 . . . . . 6
13 elom 6489 . . . . . 6
14 elom 6489 . . . . . 6
1512, 13, 143imtr4g 263 . . . . 5
1615imp 420 . . . 4
1716ax-gen 1570 . . 3
181, 17mpgbir 1574 . 2
19 omsson 6490 . 2
20 ordon 6404 . 2
21 trssord 4757 . 2
2218, 19, 20, 21mp3an 1287 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  A.wal 1564  e.wcel 1732  C_wss 3365  Trwtr 4411  Ordword 4739   con0 4740  Limwlim 4741   com 6486
This theorem is referenced by:  elnn  6496  omon  6497  limom  6501  ssnlim  6504  peano5  6509  nnarcl  7021  nnawordex  7042  oaabslem  7048  oaabs2  7050  omabslem  7051  onomeneq  7461  ominf  7486  findcard3  7516  nnsdomg  7532  dffi3  7603  wofib  7681  alephgeom  8134  iscard3  8145  iunfictbso  8166  unctb  8256  ackbij2lem1  8270  ackbij1lem3  8273  ackbij1lem18  8288  ackbij2  8294  cflim2  8314  fin23lem26  8376  fin23lem23  8377  fin23lem27  8379  fin67  8446  alephexp1  8625  pwfseqlem3  8706  pwcdandom  8713  winainflem  8739  wunex2  8784  om2uzoi  11627  ltweuz  11633  fz1isolem  12061  mreexexd  14427  1stcrestlem  18530  omsinds  26833  hfuni  27464  hfninf  27466
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pr 4554  ax-un 6382
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-ral 2764  df-rex 2765  df-rab 2768  df-v 3017  df-sbc 3225  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-pss 3381  df-nul 3674  df-if 3826  df-sn 3915  df-pr 3916  df-tp 3917  df-op 3918  df-uni 4118  df-br 4319  df-opab 4377  df-tr 4412  df-eprel 4653  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-om 6487
  Copyright terms: Public domain W3C validator