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

Theorem 1on 6570
Description: Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
1on  |-  1o  e.  On

Proof of Theorem 1on
StepHypRef Expression
1 df-1o 6563 . 2  |-  1o  =  suc  (/)
2 0elon 4524 . . 3  |-  (/)  e.  On
32onsuci 4708 . 2  |-  suc  (/)  e.  On
41, 3eqeltri 2428 1  |-  1o  e.  On
Colors of variables: wff set class
Syntax hints:    e. wcel 1710   (/)c0 3531   Oncon0 4471   suc csuc 4473   1oc1o 6556
This theorem is referenced by:  2on  6571  ondif2  6585  2oconcl  6586  fnoe  6593  oev  6597  oe0  6605  oev2  6606  oesuclem  6608  oecl  6620  o1p1e2  6623  om1r  6625  oe1m  6627  omword1  6655  omword2  6656  omlimcl  6660  oneo  6663  oewordi  6673  oelim2  6677  oeoa  6679  oeoe  6681  oeeui  6684  oaabs2  6727  endisj  7034  sdom1  7147  sucxpdom  7157  oancom  7439  cnfcom3lem  7493  pm54.43lem  7719  pm54.43  7720  infxpenc  7732  infxpenc2  7736  uncdadom  7884  cdaun  7885  cdaen  7886  cda1dif  7889  pm110.643  7890  pm110.643ALT  7891  cdacomen  7894  cdaassen  7895  xpcdaen  7896  mapcdaen  7897  cdaxpdom  7902  cdafi  7903  cdainf  7905  infcda1  7906  pwcda1  7907  pwcdadom  7929  cfsuc  7970  isfin4-3  8028  dcomex  8160  pwcfsdom  8292  pwxpndom2  8374  wunex2  8447  wuncval2  8456  tsk2  8474  sadcf  12735  sadcp1  12737  xpscg  13553  xpscfn  13554  xpsc0  13555  xpsc1  13556  xpsfrnel  13558  xpsfrnel2  13560  xpsle  13576  efgmnvl  15116  efgi1  15123  frgpuptinv  15173  frgpnabllem1  15254  dmdprdpr  15377  dprdpr  15378  psr1crng  16359  psr1assa  16360  psr1tos  16361  psr1bas  16363  vr1cl2  16365  ply1lss  16368  ply1subrg  16369  coe1fval3  16382  ressply1bas2  16399  ressply1add  16401  ressply1mul  16402  ressply1vsca  16403  subrgply1  16404  00ply1bas  16411  ply1plusgfvi  16413  psr1rng  16418  psr1lmod  16420  psr1sca  16421  ply1ascl  16428  subrg1ascl  16429  subrg1asclcl  16430  subrgvr1  16431  subrgvr1cl  16432  coe1z  16433  coe1mul2lem1  16437  coe1mul2  16439  coe1tm  16442  xkofvcn  17478  xpstopnlem1  17600  xpstopnlem2  17602  ufildom1  17717  xpsdsval  18041  evl1val  19509  evl1rhm  19510  evl1sca  19511  evl1var  19513  mpfpf1  19532  pf1mpf  19533  pf1ind  19536  deg1z  19571  deg1addle  19585  deg1vscale  19588  deg1vsca  19589  deg1mulle2  19593  deg1le0  19595  ply1nzb  19606  sltval2  24868  nofv  24869  noxp1o  24878  sltsolem1  24880  bdayfo  24887  nobnddown  24913  rankeq1o  25360  ssoninhaus  25446  onint1  25447  pw2f1ocnv  26453  wepwsolem  26461  pwfi2f1o  26583
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pr 4293  ax-un 4591
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3907  df-br 4103  df-opab 4157  df-tr 4193  df-eprel 4384  df-po 4393  df-so 4394  df-fr 4431  df-we 4433  df-ord 4474  df-on 4475  df-suc 4477  df-1o 6563
  Copyright terms: Public domain W3C validator