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

Theorem 1on 7139
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 7132 . 2  |-  1o  =  suc  (/)
2 0elon 4921 . . 3  |-  (/)  e.  On
32onsuci 6658 . 2  |-  suc  (/)  e.  On
41, 3eqeltri 2527 1  |-  1o  e.  On
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1804   (/)c0 3770   Oncon0 4868   suc csuc 4870   1oc1o 7125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-tr 4531  df-eprel 4781  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-suc 4874  df-1o 7132
This theorem is referenced by:  2on  7140  ondif2  7154  2oconcl  7155  fnoe  7162  oev  7166  oe0  7174  oev2  7175  oesuclem  7177  oecl  7189  o1p1e2  7192  om1r  7194  oe1m  7196  omword1  7224  omword2  7225  omlimcl  7229  oneo  7232  oewordi  7242  oelim2  7246  oeoa  7248  oeoe  7250  oeeui  7253  oaabs2  7296  endisj  7606  sdom1  7721  sucxpdom  7731  oancom  8071  cnfcom3lem  8150  cnfcom3lemOLD  8158  pm54.43lem  8383  pm54.43  8384  infxpenc  8398  infxpenc2  8402  infxpencOLD  8403  infxpenc2OLD  8406  uncdadom  8554  cdaun  8555  cdaen  8556  cda1dif  8559  pm110.643  8560  pm110.643ALT  8561  cdacomen  8564  cdaassen  8565  xpcdaen  8566  mapcdaen  8567  cdaxpdom  8572  cdafi  8573  cdainf  8575  infcda1  8576  pwcda1  8577  pwcdadom  8599  cfsuc  8640  isfin4-3  8698  dcomex  8830  pwcfsdom  8961  pwxpndom2  9046  wunex2  9119  wuncval2  9128  tsk2  9146  sadcf  13980  sadcp1  13982  xpscg  14832  xpscfn  14833  xpsc0  14834  xpsc1  14835  xpsfrnel  14837  xpsfrnel2  14839  xpsle  14855  efgmnvl  16606  efgi1  16613  frgpuptinv  16663  frgpnabllem1  16751  dmdprdpr  16972  dprdpr  16973  psr1crng  18100  psr1assa  18101  psr1tos  18102  psr1bas  18104  vr1cl2  18106  ply1lss  18109  ply1subrg  18110  coe1fval3  18121  ressply1bas2  18143  ressply1add  18145  ressply1mul  18146  ressply1vsca  18147  subrgply1  18148  00ply1bas  18155  ply1plusgfvi  18157  psr1ring  18162  psr1lmod  18164  psr1sca  18165  ply1ascl  18173  subrg1ascl  18174  subrg1asclcl  18175  subrgvr1  18176  subrgvr1cl  18177  coe1z  18178  coe1mul2lem1  18182  coe1mul2  18184  coe1tm  18188  evls1val  18231  evls1rhm  18233  evls1sca  18234  evl1val  18239  evl1rhm  18242  evl1sca  18244  evl1var  18246  evls1var  18248  mpfpf1  18261  pf1mpf  18262  pf1ind  18265  xkofvcn  20058  xpstopnlem1  20183  xpstopnlem2  20185  ufildom1  20300  xpsdsval  20757  deg1z  22360  deg1addle  22375  deg1vscale  22378  deg1vsca  22379  deg1mulle2  22383  deg1le0  22385  ply1nzb  22396  sltval2  29391  nofv  29392  noxp1o  29401  sltsolem1  29403  bdayfo  29410  nobnddown  29436  rankeq1o  29803  ssoninhaus  29888  onint1  29889  pw2f1ocnv  30954  wepwsolem  30962  pwfi2f1o  31019  ply1ass23l  32717
  Copyright terms: Public domain W3C validator