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

Theorem eloni 4811
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 4809 . 2
21ibi 241 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1757  Ordword 4800   con0 4801
This theorem is referenced by:  elon2  4812  onelon  4826  onin  4832  ontri1  4835  onfr  4840  onelpss  4841  onsseleq  4842  onelss  4843  ontr1  4847  ontr2  4848  ordunidif  4849  on0eln0  4856  ordsssuc  4887  onsssuc  4888  onnbtwn  4892  suc11  4904  onordi  4905  onssneli  4910  ordon  6478  ordeleqon  6484  onss  6486  ordsuc  6509  onpwsuc  6511  onpsssuc  6514  onsucmin  6516  ordunpr  6521  ordunisuc  6527  onsucuni2  6529  onuninsuci  6535  ordunisuc2  6539  ordzsl  6540  onzsl  6541  nlimon  6546  tfinds  6554  tfindsg2  6556  nnord  6568  onfununi  6886  smo11  6909  smoord  6910  smoword  6911  smogt  6912  tfrlem1  6919  tfrlem9a  6929  tfrlem15  6935  tz7.44-2  6947  tz7.48lem  6980  oe0m1  7045  oaordi  7069  oaord  7070  oacan  7071  oawordri  7073  oalimcl  7083  oaass  7084  omord2  7090  omcan  7092  omwordi  7094  omword1  7096  omword2  7097  om00  7098  omlimcl  7101  omass  7103  omeulem2  7106  omopth2  7107  oen0  7109  oeord  7111  oecan  7112  oewordi  7114  oeworde  7116  oelimcl  7123  oeeulem  7124  oeeui  7125  nnarcl  7139  nnawordi  7144  nnawordex  7160  oaabs2  7168  omabs  7170  omsmo  7177  omxpenlem  7496  infensuc  7573  onomeneq  7585  ordiso  7815  ordtypelem2  7818  hartogslem1  7841  cantnflt  7965  cantnfp1lem3  7973  cantnfp1  7974  oemapso  7975  oemapvali  7977  cantnflem1d  7981  cantnflem1  7982  cantnf  7986  oemapwe  7987  cantnffval2  7988  cantnfltOLD  7995  cantnfp1lem3OLD  7999  cantnfp1OLD  8000  cantnflem1dOLD  8004  cantnflem1OLD  8005  cantnfOLD  8008  oemapweOLD  8009  cantnffval2OLD  8010  cnfcom  8018  cnfcomOLD  8026  r111  8067  r1ordg  8070  rankonidlem  8120  bndrank  8133  r1pw  8137  r1pwOLD  8138  rankbnd2  8161  tcrank  8176  cardprclem  8234  carduni  8236  cardmin2  8253  infxpenlem  8265  alephdom  8336  alephdom2  8342  cardaleph  8344  iscard3  8348  alephfp  8363  dfac12lem1  8397  dfac12lem2  8398  dfac12lem3  8399  cflim2  8517  cofsmo  8523  cfsmolem  8524  coftr  8527  cfcof  8528  fin67  8649  hsmexlem5  8684  zorn2lem6  8755  ttukeylem3  8765  ttukeylem5  8767  ttukeylem6  8768  ttukeylem7  8769  winainflem  8945  r1limwun  8988  r1wunlim  8989  tsksuc  9014  inar1  9027  gruina  9070  grur1a  9071  grur1  9072  dfrdg2  27727  poseq  27832  soseq  27833  nodmord  27912  nodenselem5  27944  nofulllem5  27965  ontgval  28395  ontgsucval  28396  onsuctopon  28398  onintopsscon  28404  onsuct0  28405  aomclem4  29532  aomclem5  29533  onfrALTlem3  31533  onfrALTlem2  31535  onfrALTlem3VD  31904  onfrALTlem2VD  31906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ral 2797  df-rex 2798  df-v 3054  df-in 3417  df-ss 3424  df-uni 4174  df-tr 4468  df-po 4723  df-so 4724  df-fr 4761  df-we 4763  df-ord 4804  df-on 4805
  Copyright terms: Public domain W3C validator