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

Theorem eloni 4893
Description: An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
Assertion
Ref Expression
eloni

Proof of Theorem eloni
StepHypRef Expression
1 elong 4891 . 2
21ibi 241 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  Ordword 4882   con0 4883
This theorem is referenced by:  elon2  4894  onelon  4908  onin  4914  ontri1  4917  onfr  4922  onelpss  4923  onsseleq  4924  onelss  4925  ontr1  4929  ontr2  4930  ordunidif  4931  on0eln0  4938  ordsssuc  4969  onsssuc  4970  onnbtwn  4974  suc11  4986  onordi  4987  onssneli  4992  ordon  6618  ordeleqon  6624  onss  6626  ordsuc  6649  onpwsuc  6651  onpsssuc  6654  onsucmin  6656  ordunpr  6661  ordunisuc  6667  onsucuni2  6669  onuninsuci  6675  ordunisuc2  6679  ordzsl  6680  onzsl  6681  nlimon  6686  tfinds  6694  tfindsg2  6696  nnord  6708  onfununi  7031  smo11  7054  smoord  7055  smoword  7056  smogt  7057  tfrlem1  7064  tfrlem9a  7074  tfrlem15  7080  tz7.44-2  7092  tz7.48lem  7125  oe0m1  7190  oaordi  7214  oaord  7215  oacan  7216  oawordri  7218  oalimcl  7228  oaass  7229  omord2  7235  omcan  7237  omwordi  7239  omword1  7241  omword2  7242  om00  7243  omlimcl  7246  omass  7248  omeulem2  7251  omopth2  7252  oen0  7254  oeord  7256  oecan  7257  oewordi  7259  oeworde  7261  oelimcl  7268  oeeulem  7269  oeeui  7270  nnarcl  7284  nnawordi  7289  nnawordex  7305  oaabs2  7313  omabs  7315  omsmo  7322  omxpenlem  7638  infensuc  7715  onomeneq  7727  ordiso  7962  ordtypelem2  7965  hartogslem1  7988  cantnflt  8112  cantnfp1lem3  8120  cantnfp1  8121  oemapso  8122  oemapvali  8124  cantnflem1d  8128  cantnflem1  8129  cantnf  8133  oemapwe  8134  cantnffval2  8135  cantnfltOLD  8142  cantnfp1lem3OLD  8146  cantnfp1OLD  8147  cantnflem1dOLD  8151  cantnflem1OLD  8152  cantnfOLD  8155  oemapweOLD  8156  cantnffval2OLD  8157  cnfcom  8165  cnfcomOLD  8173  r111  8214  r1ordg  8217  rankonidlem  8267  bndrank  8280  r1pw  8284  r1pwOLD  8285  rankbnd2  8308  tcrank  8323  cardprclem  8381  carduni  8383  cardmin2  8400  infxpenlem  8412  alephdom  8483  alephdom2  8489  cardaleph  8491  iscard3  8495  alephfp  8510  dfac12lem1  8544  dfac12lem2  8545  dfac12lem3  8546  cflim2  8664  cofsmo  8670  cfsmolem  8671  coftr  8674  cfcof  8675  fin67  8796  hsmexlem5  8831  zorn2lem6  8902  ttukeylem3  8912  ttukeylem5  8914  ttukeylem6  8915  ttukeylem7  8916  winainflem  9092  r1limwun  9135  r1wunlim  9136  tsksuc  9161  inar1  9174  gruina  9217  grur1a  9218  grur1  9219  dfrdg2  29228  poseq  29333  soseq  29334  nodmord  29413  nodenselem5  29445  nofulllem5  29466  ontgval  29896  ontgsucval  29897  onsuctopon  29899  onintopsscon  29905  onsuct0  29906  aomclem4  31003  aomclem5  31004  onfrALTlem3  33316  onfrALTlem2  33318  onfrALTlem3VD  33687  onfrALTlem2VD  33689
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-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-in 3482  df-ss 3489  df-uni 4250  df-tr 4546  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887
  Copyright terms: Public domain W3C validator