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

Theorem 1on 6669
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 6662 . 2  |-  1o  =  suc  (/)
2 0elon 4577 . . 3  |-  (/)  e.  On
32onsuci 4760 . 2  |-  suc  (/)  e.  On
41, 3eqeltri 2459 1  |-  1o  e.  On
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   (/)c0 3573   Oncon0 4524   suc csuc 4526   1oc1o 6655
This theorem is referenced by:  2on  6670  ondif2  6684  2oconcl  6685  fnoe  6692  oev  6696  oe0  6704  oev2  6705  oesuclem  6707  oecl  6719  o1p1e2  6722  om1r  6724  oe1m  6726  omword1  6754  omword2  6755  omlimcl  6759  oneo  6762  oewordi  6772  oelim2  6776  oeoa  6778  oeoe  6780  oeeui  6783  oaabs2  6826  endisj  7133  sdom1  7246  sucxpdom  7256  oancom  7541  cnfcom3lem  7595  pm54.43lem  7821  pm54.43  7822  infxpenc  7834  infxpenc2  7838  uncdadom  7986  cdaun  7987  cdaen  7988  cda1dif  7991  pm110.643  7992  pm110.643ALT  7993  cdacomen  7996  cdaassen  7997  xpcdaen  7998  mapcdaen  7999  cdaxpdom  8004  cdafi  8005  cdainf  8007  infcda1  8008  pwcda1  8009  pwcdadom  8031  cfsuc  8072  isfin4-3  8130  dcomex  8262  pwcfsdom  8393  pwxpndom2  8475  wunex2  8548  wuncval2  8557  tsk2  8575  sadcf  12894  sadcp1  12896  xpscg  13712  xpscfn  13713  xpsc0  13714  xpsc1  13715  xpsfrnel  13717  xpsfrnel2  13719  xpsle  13735  efgmnvl  15275  efgi1  15282  frgpuptinv  15332  frgpnabllem1  15413  dmdprdpr  15536  dprdpr  15537  psr1crng  16514  psr1assa  16515  psr1tos  16516  psr1bas  16518  vr1cl2  16520  ply1lss  16523  ply1subrg  16524  coe1fval3  16535  ressply1bas2  16551  ressply1add  16553  ressply1mul  16554  ressply1vsca  16555  subrgply1  16556  00ply1bas  16563  ply1plusgfvi  16565  psr1rng  16570  psr1lmod  16572  psr1sca  16573  ply1ascl  16580  subrg1ascl  16581  subrg1asclcl  16582  subrgvr1  16583  subrgvr1cl  16584  coe1z  16585  coe1mul2lem1  16589  coe1mul2  16591  coe1tm  16594  xkofvcn  17639  xpstopnlem1  17764  xpstopnlem2  17766  ufildom1  17881  xpsdsval  18321  evl1val  19817  evl1rhm  19818  evl1sca  19819  evl1var  19821  mpfpf1  19840  pf1mpf  19841  pf1ind  19844  deg1z  19879  deg1addle  19893  deg1vscale  19896  deg1vsca  19897  deg1mulle2  19901  deg1le0  19903  ply1nzb  19914  sltval2  25336  nofv  25337  noxp1o  25346  sltsolem1  25348  bdayfo  25355  nobnddown  25381  rankeq1o  25828  ssoninhaus  25914  onint1  25915  pw2f1ocnv  26801  wepwsolem  26809  pwfi2f1o  26931
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pr 4346  ax-un 4643
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-sbc 3107  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-pss 3281  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-tp 3767  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-tr 4246  df-eprel 4437  df-po 4446  df-so 4447  df-fr 4484  df-we 4486  df-ord 4527  df-on 4528  df-suc 4530  df-1o 6662
  Copyright terms: Public domain W3C validator