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

Theorem 1on 6915
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 6908 . 2  |-  1o  =  suc  (/)
2 0elon 4759 . . 3  |-  (/)  e.  On
32onsuci 6438 . 2  |-  suc  (/)  e.  On
41, 3eqeltri 2503 1  |-  1o  e.  On
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755   (/)c0 3625   Oncon0 4706   suc csuc 4708   1oc1o 6901
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-tr 4374  df-eprel 4619  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-suc 4712  df-1o 6908
This theorem is referenced by:  2on  6916  ondif2  6930  2oconcl  6931  fnoe  6938  oev  6942  oe0  6950  oev2  6951  oesuclem  6953  oecl  6965  o1p1e2  6968  om1r  6970  oe1m  6972  omword1  7000  omword2  7001  omlimcl  7005  oneo  7008  oewordi  7018  oelim2  7022  oeoa  7024  oeoe  7026  oeeui  7029  oaabs2  7072  endisj  7386  sdom1  7500  sucxpdom  7510  oancom  7845  cnfcom3lem  7924  cnfcom3lemOLD  7932  pm54.43lem  8157  pm54.43  8158  infxpenc  8172  infxpenc2  8176  infxpencOLD  8177  infxpenc2OLD  8180  uncdadom  8328  cdaun  8329  cdaen  8330  cda1dif  8333  pm110.643  8334  pm110.643ALT  8335  cdacomen  8338  cdaassen  8339  xpcdaen  8340  mapcdaen  8341  cdaxpdom  8346  cdafi  8347  cdainf  8349  infcda1  8350  pwcda1  8351  pwcdadom  8373  cfsuc  8414  isfin4-3  8472  dcomex  8604  pwcfsdom  8735  pwxpndom2  8820  wunex2  8893  wuncval2  8902  tsk2  8920  sadcf  13632  sadcp1  13634  xpscg  14479  xpscfn  14480  xpsc0  14481  xpsc1  14482  xpsfrnel  14484  xpsfrnel2  14486  xpsle  14502  efgmnvl  16191  efgi1  16198  frgpuptinv  16248  frgpnabllem1  16331  dmdprdpr  16522  dprdpr  16523  psr1crng  17542  psr1assa  17543  psr1tos  17544  psr1bas  17546  vr1cl2  17548  ply1lss  17551  ply1subrg  17552  coe1fval3  17563  ressply1bas2  17581  ressply1add  17583  ressply1mul  17584  ressply1vsca  17585  subrgply1  17586  00ply1bas  17593  ply1plusgfvi  17595  psr1rng  17600  psr1lmod  17602  psr1sca  17603  ply1ascl  17610  subrg1ascl  17611  subrg1asclcl  17612  subrgvr1  17613  subrgvr1cl  17614  coe1z  17615  coe1mul2lem1  17619  coe1mul2  17621  coe1tm  17624  xkofvcn  19099  xpstopnlem1  19224  xpstopnlem2  19226  ufildom1  19341  xpsdsval  19798  evl1val  21379  evl1rhm  21380  evl1sca  21381  evl1var  21383  mpfpf1  21402  pf1mpf  21403  pf1ind  21406  deg1z  21443  deg1addle  21458  deg1vscale  21461  deg1vsca  21462  deg1mulle2  21466  deg1le0  21468  ply1nzb  21479  sltval2  27644  nofv  27645  noxp1o  27654  sltsolem1  27656  bdayfo  27663  nobnddown  27689  rankeq1o  28056  ssoninhaus  28142  onint1  28143  pw2f1ocnv  29231  wepwsolem  29239  pwfi2f1o  29296
  Copyright terms: Public domain W3C validator