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

Theorem onelon 4908
Description: An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.)
Assertion
Ref Expression
onelon

Proof of Theorem onelon
StepHypRef Expression
1 eloni 4893 . 2
2 ordelon 4907 . 2
31, 2sylan 471 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  Ordword 4882   con0 4883
This theorem is referenced by:  oneli  4990  ssorduni  6621  unon  6666  tfindsg2  6696  dfom2  6702  ordom  6709  onfununi  7031  onnseq  7034  tz7.48-2  7126  tz7.49  7129  oalim  7201  omlim  7202  oelim  7203  oaordi  7214  oalimcl  7228  oaass  7229  omordi  7234  omlimcl  7246  odi  7247  omass  7248  omeulem1  7250  omeulem2  7251  omopth2  7252  oewordri  7260  oeordsuc  7262  oelimcl  7268  oeeui  7270  oaabs2  7313  omabs  7315  omxpenlem  7638  hartogs  7990  card2on  8001  cantnfle  8111  cantnflt  8112  cantnfp1lem2  8119  cantnfp1lem3  8120  cantnfp1  8121  oemapvali  8124  cantnflem1b  8126  cantnflem1c  8127  cantnflem1d  8128  cantnflem1  8129  cantnflem2  8130  cantnflem3  8131  cantnflem4  8132  cantnf  8133  cantnfleOLD  8141  cantnfltOLD  8142  cantnfp1lem2OLD  8145  cantnfp1lem3OLD  8146  cantnfp1OLD  8147  cantnflem1bOLD  8149  cantnflem1cOLD  8150  cantnflem1dOLD  8151  cantnflem1OLD  8152  cantnflem3OLD  8153  cantnflem4OLD  8154  cantnfOLD  8155  cnfcomlem  8164  cnfcom3lem  8168  cnfcom3  8169  cnfcomlemOLD  8172  cnfcom3lemOLD  8176  cnfcom3OLD  8177  r1ordg  8217  r1val3  8277  tskwe  8352  iscard  8377  cardmin2  8400  infxpenlem  8412  infxpenc2lem2  8418  infxpenc2lem2OLD  8422  alephordi  8476  alephord2i  8479  alephle  8490  cardaleph  8491  cfub  8650  cfsmolem  8671  zorn2lem5  8901  zorn2lem6  8902  ttukeylem6  8915  ttukeylem7  8916  ondomon  8959  cardmin  8960  alephval2  8968  alephreg  8978  smobeth  8982  winainflem  9092  inar1  9174  inatsk  9177  dfrdg2  29228  sltval2  29416  sltres  29424  nodenselem5  29445  nodenselem7  29447  nobndlem6  29457  nobndup  29460  dfrdg4  29600  ontopbas  29893  onpsstopbas  29895  onint1  29914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-tr 4546  df-eprel 4796  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887
  Copyright terms: Public domain W3C validator