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

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

Proof of Theorem 1on
StepHypRef Expression
1 df-1o 8089 . 2 1o = suc ∅
2 0elon 6222 . . 3 ∅ ∈ On
32onsuci 7538 . 2 suc ∅ ∈ On
41, 3eqeltri 2910 1 1o ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  c0 4265  Oncon0 6169  suc csuc 6171  1oc1o 8082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307  ax-un 7446
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-tr 5149  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-ord 6172  df-on 6173  df-suc 6175  df-1o 8089
This theorem is referenced by:  1oex  8097  2on  8098  ondif2  8114  2oconcl  8115  fnoe  8122  oesuclem  8137  oecl  8149  o1p1e2  8152  o2p2e4OLD  8154  om1r  8156  oe1m  8158  omword1  8186  omword2  8187  omlimcl  8191  oneo  8194  oewordi  8204  oelim2  8208  oeoa  8210  oeoe  8212  oeeui  8215  oaabs2  8259  enpr2d  8584  sucxpdom  8715  oancom  9102  cnfcom3lem  9154  pm54.43lem  9417  pm54.43  9418  infxpenc  9433  infxpenc2  9437  undjudom  9582  endjudisj  9583  djuen  9584  dju1p1e2  9588  dju1p1e2ALT  9589  xpdjuen  9594  mapdjuen  9595  djuxpdom  9600  djufi  9601  djuinf  9603  infdju1  9604  pwdju1  9605  pwdjudom  9627  isfin4p1  9726  pwxpndom2  10076  wunex2  10149  wuncval2  10158  tsk2  10176  efgmnvl  18831  frgpnabllem1  18984  dmdprdpr  19162  dprdpr  19163  psr1crng  20814  psr1assa  20815  psr1tos  20816  psr1bas  20818  vr1cl2  20820  ply1lss  20823  ply1subrg  20824  ressply1bas2  20855  ressply1add  20857  ressply1mul  20858  ressply1vsca  20859  subrgply1  20860  ply1plusgfvi  20869  psr1ring  20874  psr1lmod  20876  psr1sca  20877  ply1ascl  20885  subrg1ascl  20886  subrg1asclcl  20887  subrgvr1  20888  subrgvr1cl  20889  coe1z  20890  coe1mul2lem1  20894  coe1mul2  20896  coe1tm  20900  evls1val  20942  evls1rhm  20944  evls1sca  20945  evl1val  20951  evl1rhm  20954  evl1sca  20956  evl1var  20958  evls1var  20960  mpfpf1  20973  pf1mpf  20974  pf1ind  20977  xkofvcn  22287  xpstopnlem1  22412  ufildom1  22529  deg1z  24686  deg1addle  24700  deg1vscale  24703  deg1vsca  24704  deg1mulle2  24708  deg1le0  24710  ply1nzb  24721  sltval2  33237  noextendlt  33250  sltsolem1  33254  nosepnelem  33258  nolt02o  33273  rankeq1o  33706  ssoninhaus  33870  onint1  33871  1oequni2o  34746  finxp1o  34770  finxpreclem3  34771  finxpreclem4  34772  finxpreclem5  34773  finxpsuclem  34775  pw2f1ocnv  39908  wepwsolem  39916  pwfi2f1o  39970  sn1dom  40164  pr2dom  40165  tr3dom  40166  clsk1indlem4  40680  ply1ass23l  44729
  Copyright terms: Public domain W3C validator