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

Theorem 1on 7127
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 7120 . 2  |-  1o  =  suc  (/)
2 0elon 4924 . . 3  |-  (/)  e.  On
32onsuci 6644 . 2  |-  suc  (/)  e.  On
41, 3eqeltri 2544 1  |-  1o  e.  On
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1762   (/)c0 3778   Oncon0 4871   suc csuc 4873   1oc1o 7113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679  ax-un 6567
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-pss 3485  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-tp 4025  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-tr 4534  df-eprel 4784  df-po 4793  df-so 4794  df-fr 4831  df-we 4833  df-ord 4874  df-on 4875  df-suc 4877  df-1o 7120
This theorem is referenced by:  2on  7128  ondif2  7142  2oconcl  7143  fnoe  7150  oev  7154  oe0  7162  oev2  7163  oesuclem  7165  oecl  7177  o1p1e2  7180  om1r  7182  oe1m  7184  omword1  7212  omword2  7213  omlimcl  7217  oneo  7220  oewordi  7230  oelim2  7234  oeoa  7236  oeoe  7238  oeeui  7241  oaabs2  7284  endisj  7594  sdom1  7709  sucxpdom  7719  oancom  8057  cnfcom3lem  8136  cnfcom3lemOLD  8144  pm54.43lem  8369  pm54.43  8370  infxpenc  8384  infxpenc2  8388  infxpencOLD  8389  infxpenc2OLD  8392  uncdadom  8540  cdaun  8541  cdaen  8542  cda1dif  8545  pm110.643  8546  pm110.643ALT  8547  cdacomen  8550  cdaassen  8551  xpcdaen  8552  mapcdaen  8553  cdaxpdom  8558  cdafi  8559  cdainf  8561  infcda1  8562  pwcda1  8563  pwcdadom  8585  cfsuc  8626  isfin4-3  8684  dcomex  8816  pwcfsdom  8947  pwxpndom2  9032  wunex2  9105  wuncval2  9114  tsk2  9132  sadcf  13951  sadcp1  13953  xpscg  14802  xpscfn  14803  xpsc0  14804  xpsc1  14805  xpsfrnel  14807  xpsfrnel2  14809  xpsle  14825  efgmnvl  16521  efgi1  16528  frgpuptinv  16578  frgpnabllem1  16661  dmdprdpr  16881  dprdpr  16882  psr1crng  17990  psr1assa  17991  psr1tos  17992  psr1bas  17994  vr1cl2  17996  ply1lss  17999  ply1subrg  18000  coe1fval3  18011  ressply1bas2  18033  ressply1add  18035  ressply1mul  18036  ressply1vsca  18037  subrgply1  18038  00ply1bas  18045  ply1plusgfvi  18047  psr1rng  18052  psr1lmod  18054  psr1sca  18055  ply1ascl  18063  subrg1ascl  18064  subrg1asclcl  18065  subrgvr1  18066  subrgvr1cl  18067  coe1z  18068  coe1mul2lem1  18072  coe1mul2  18074  coe1tm  18078  evls1val  18121  evls1rhm  18123  evls1sca  18124  evl1val  18129  evl1rhm  18132  evl1sca  18134  evl1var  18136  evls1var  18138  mpfpf1  18151  pf1mpf  18152  pf1ind  18155  xkofvcn  19913  xpstopnlem1  20038  xpstopnlem2  20040  ufildom1  20155  xpsdsval  20612  deg1z  22215  deg1addle  22230  deg1vscale  22233  deg1vsca  22234  deg1mulle2  22238  deg1le0  22240  ply1nzb  22251  sltval2  28979  nofv  28980  noxp1o  28989  sltsolem1  28991  bdayfo  28998  nobnddown  29024  rankeq1o  29391  ssoninhaus  29476  onint1  29477  pw2f1ocnv  30572  wepwsolem  30580  pwfi2f1o  30637  ply1ass23l  31930
  Copyright terms: Public domain W3C validator