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

Theorem 1on 6690
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 6683 . 2  |-  1o  =  suc  (/)
2 0elon 4594 . . 3  |-  (/)  e.  On
32onsuci 4777 . 2  |-  suc  (/)  e.  On
41, 3eqeltri 2474 1  |-  1o  e.  On
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   (/)c0 3588   Oncon0 4541   suc csuc 4543   1oc1o 6676
This theorem is referenced by:  2on  6691  ondif2  6705  2oconcl  6706  fnoe  6713  oev  6717  oe0  6725  oev2  6726  oesuclem  6728  oecl  6740  o1p1e2  6743  om1r  6745  oe1m  6747  omword1  6775  omword2  6776  omlimcl  6780  oneo  6783  oewordi  6793  oelim2  6797  oeoa  6799  oeoe  6801  oeeui  6804  oaabs2  6847  endisj  7154  sdom1  7267  sucxpdom  7277  oancom  7562  cnfcom3lem  7616  pm54.43lem  7842  pm54.43  7843  infxpenc  7855  infxpenc2  7859  uncdadom  8007  cdaun  8008  cdaen  8009  cda1dif  8012  pm110.643  8013  pm110.643ALT  8014  cdacomen  8017  cdaassen  8018  xpcdaen  8019  mapcdaen  8020  cdaxpdom  8025  cdafi  8026  cdainf  8028  infcda1  8029  pwcda1  8030  pwcdadom  8052  cfsuc  8093  isfin4-3  8151  dcomex  8283  pwcfsdom  8414  pwxpndom2  8496  wunex2  8569  wuncval2  8578  tsk2  8596  sadcf  12920  sadcp1  12922  xpscg  13738  xpscfn  13739  xpsc0  13740  xpsc1  13741  xpsfrnel  13743  xpsfrnel2  13745  xpsle  13761  efgmnvl  15301  efgi1  15308  frgpuptinv  15358  frgpnabllem1  15439  dmdprdpr  15562  dprdpr  15563  psr1crng  16540  psr1assa  16541  psr1tos  16542  psr1bas  16544  vr1cl2  16546  ply1lss  16549  ply1subrg  16550  coe1fval3  16561  ressply1bas2  16577  ressply1add  16579  ressply1mul  16580  ressply1vsca  16581  subrgply1  16582  00ply1bas  16589  ply1plusgfvi  16591  psr1rng  16596  psr1lmod  16598  psr1sca  16599  ply1ascl  16606  subrg1ascl  16607  subrg1asclcl  16608  subrgvr1  16609  subrgvr1cl  16610  coe1z  16611  coe1mul2lem1  16615  coe1mul2  16617  coe1tm  16620  xkofvcn  17669  xpstopnlem1  17794  xpstopnlem2  17796  ufildom1  17911  xpsdsval  18364  evl1val  19901  evl1rhm  19902  evl1sca  19903  evl1var  19905  mpfpf1  19924  pf1mpf  19925  pf1ind  19928  deg1z  19963  deg1addle  19977  deg1vscale  19980  deg1vsca  19981  deg1mulle2  19985  deg1le0  19987  ply1nzb  19998  sltval2  25524  nofv  25525  noxp1o  25534  sltsolem1  25536  bdayfo  25543  nobnddown  25569  rankeq1o  26016  ssoninhaus  26102  onint1  26103  pw2f1ocnv  26998  wepwsolem  27006  pwfi2f1o  27128
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 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363  ax-un 4660
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 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-tr 4263  df-eprel 4454  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-suc 4547  df-1o 6683
  Copyright terms: Public domain W3C validator