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

Theorem 1on 7527
Description: Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
1on 1𝑜 ∈ On

Proof of Theorem 1on
StepHypRef Expression
1 df-1o 7520 . 2 1𝑜 = suc ∅
2 0elon 5747 . . 3 ∅ ∈ On
32onsuci 7000 . 2 suc ∅ ∈ On
41, 3eqeltri 2694 1 1𝑜 ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  c0 3897  Oncon0 5692  suc csuc 5694  1𝑜c1o 7513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877  ax-un 6914
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-br 4624  df-opab 4684  df-tr 4723  df-eprel 4995  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-ord 5695  df-on 5696  df-suc 5698  df-1o 7520
This theorem is referenced by:  2on  7528  ondif2  7542  2oconcl  7543  fnoe  7550  oev  7554  oe0  7562  oev2  7563  oesuclem  7565  oecl  7577  o1p1e2  7580  o2p2e4  7581  om1r  7583  oe1m  7585  omword1  7613  omword2  7614  omlimcl  7618  oneo  7621  oewordi  7631  oelim2  7635  oeoa  7637  oeoe  7639  oeeui  7642  oaabs2  7685  endisj  8007  sdom1  8120  sucxpdom  8129  oancom  8508  cnfcom3lem  8560  pm54.43lem  8785  pm54.43  8786  infxpenc  8801  infxpenc2  8805  uncdadom  8953  cdaun  8954  cdaen  8955  cda1dif  8958  pm110.643  8959  pm110.643ALT  8960  cdacomen  8963  cdaassen  8964  xpcdaen  8965  mapcdaen  8966  cdaxpdom  8971  cdafi  8972  cdainf  8974  infcda1  8975  pwcda1  8976  pwcdadom  8998  cfsuc  9039  isfin4-3  9097  dcomex  9229  pwcfsdom  9365  pwxpndom2  9447  wunex2  9520  wuncval2  9529  tsk2  9547  sadcf  15118  sadcp1  15120  xpscg  16158  xpscfn  16159  xpsc0  16160  xpsc1  16161  xpsfrnel  16163  xpsfrnel2  16165  xpsle  16181  efgmnvl  18067  efgi1  18074  frgpuptinv  18124  frgpnabllem1  18216  dmdprdpr  18388  dprdpr  18389  psr1crng  19497  psr1assa  19498  psr1tos  19499  psr1bas  19501  vr1cl2  19503  ply1lss  19506  ply1subrg  19507  coe1fval3  19518  ressply1bas2  19538  ressply1add  19540  ressply1mul  19541  ressply1vsca  19542  subrgply1  19543  00ply1bas  19550  ply1plusgfvi  19552  psr1ring  19557  psr1lmod  19559  psr1sca  19560  ply1ascl  19568  subrg1ascl  19569  subrg1asclcl  19570  subrgvr1  19571  subrgvr1cl  19572  coe1z  19573  coe1mul2lem1  19577  coe1mul2  19579  coe1tm  19583  evls1val  19625  evls1rhm  19627  evls1sca  19628  evl1val  19633  evl1rhm  19636  evl1sca  19638  evl1var  19640  evls1var  19642  mpfpf1  19655  pf1mpf  19656  pf1ind  19659  xkofvcn  21427  xpstopnlem1  21552  xpstopnlem2  21554  ufildom1  21670  xpsdsval  22126  deg1z  23785  deg1addle  23799  deg1vscale  23802  deg1vsca  23803  deg1mulle2  23807  deg1le0  23809  ply1nzb  23820  sltval2  31563  nofv  31564  noxp1o  31573  noextendlt  31579  sltsolem1  31581  bdayfo  31591  nobnddown  31617  nosepnelem  31618  nosepdmlem  31620  nosino  31628  rankeq1o  31973  ssoninhaus  32142  onint1  32143  finxp1o  32900  finxpreclem3  32901  finxpreclem4  32902  finxpreclem5  32903  finxpsuclem  32905  pw2f1ocnv  37123  wepwsolem  37131  pwfi2f1o  37185  clsk3nimkb  37859  clsk1indlem4  37863  clsk1indlem1  37864  ply1ass23l  41488
  Copyright terms: Public domain W3C validator