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

Theorem 1on 6930
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 6923 . 2  |-  1o  =  suc  (/)
2 0elon 4775 . . 3  |-  (/)  e.  On
32onsuci 6452 . 2  |-  suc  (/)  e.  On
41, 3eqeltri 2513 1  |-  1o  e.  On
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   (/)c0 3640   Oncon0 4722   suc csuc 4724   1oc1o 6916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pr 4534  ax-un 6375
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-pss 3347  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-tp 3885  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-tr 4389  df-eprel 4635  df-po 4644  df-so 4645  df-fr 4682  df-we 4684  df-ord 4725  df-on 4726  df-suc 4728  df-1o 6923
This theorem is referenced by:  2on  6931  ondif2  6945  2oconcl  6946  fnoe  6953  oev  6957  oe0  6965  oev2  6966  oesuclem  6968  oecl  6980  o1p1e2  6983  om1r  6985  oe1m  6987  omword1  7015  omword2  7016  omlimcl  7020  oneo  7023  oewordi  7033  oelim2  7037  oeoa  7039  oeoe  7041  oeeui  7044  oaabs2  7087  endisj  7401  sdom1  7515  sucxpdom  7525  oancom  7860  cnfcom3lem  7939  cnfcom3lemOLD  7947  pm54.43lem  8172  pm54.43  8173  infxpenc  8187  infxpenc2  8191  infxpencOLD  8192  infxpenc2OLD  8195  uncdadom  8343  cdaun  8344  cdaen  8345  cda1dif  8348  pm110.643  8349  pm110.643ALT  8350  cdacomen  8353  cdaassen  8354  xpcdaen  8355  mapcdaen  8356  cdaxpdom  8361  cdafi  8362  cdainf  8364  infcda1  8365  pwcda1  8366  pwcdadom  8388  cfsuc  8429  isfin4-3  8487  dcomex  8619  pwcfsdom  8750  pwxpndom2  8835  wunex2  8908  wuncval2  8917  tsk2  8935  sadcf  13652  sadcp1  13654  xpscg  14499  xpscfn  14500  xpsc0  14501  xpsc1  14502  xpsfrnel  14504  xpsfrnel2  14506  xpsle  14522  efgmnvl  16214  efgi1  16221  frgpuptinv  16271  frgpnabllem1  16354  dmdprdpr  16551  dprdpr  16552  psr1crng  17646  psr1assa  17647  psr1tos  17648  psr1bas  17650  vr1cl2  17652  ply1lss  17655  ply1subrg  17656  coe1fval3  17667  ressply1bas2  17685  ressply1add  17687  ressply1mul  17688  ressply1vsca  17689  subrgply1  17690  00ply1bas  17698  ply1plusgfvi  17700  psr1rng  17705  psr1lmod  17707  psr1sca  17708  ply1ascl  17715  subrg1ascl  17716  subrg1asclcl  17717  subrgvr1  17718  subrgvr1cl  17719  coe1z  17720  coe1mul2lem1  17724  coe1mul2  17726  coe1tm  17729  evls1val  17758  evls1rhm  17760  evls1sca  17761  evl1val  17766  evl1rhm  17769  evl1sca  17771  evl1var  17773  evls1var  17775  mpfpf1  17788  pf1mpf  17789  pf1ind  17792  xkofvcn  19260  xpstopnlem1  19385  xpstopnlem2  19387  ufildom1  19502  xpsdsval  19959  deg1z  21561  deg1addle  21576  deg1vscale  21579  deg1vsca  21580  deg1mulle2  21584  deg1le0  21586  ply1nzb  21597  sltval2  27800  nofv  27801  noxp1o  27810  sltsolem1  27812  bdayfo  27819  nobnddown  27845  rankeq1o  28212  ssoninhaus  28297  onint1  28298  pw2f1ocnv  29389  wepwsolem  29397  pwfi2f1o  29454  ply1ass23l  30831
  Copyright terms: Public domain W3C validator