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

Theorem 1on 7428
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 7421 . 2 1𝑜 = suc ∅
2 0elon 5678 . . 3 ∅ ∈ On
32onsuci 6904 . 2 suc ∅ ∈ On
41, 3eqeltri 2680 1 1𝑜 ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  c0 3870  Oncon0 5623  suc csuc 5625  1𝑜c1o 7414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pr 4825  ax-un 6821
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-sbc 3399  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-br 4575  df-opab 4635  df-tr 4672  df-eprel 4936  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-ord 5626  df-on 5627  df-suc 5629  df-1o 7421
This theorem is referenced by:  2on  7429  ondif2  7443  2oconcl  7444  fnoe  7451  oev  7455  oe0  7463  oev2  7464  oesuclem  7466  oecl  7478  o1p1e2  7481  o2p2e4  7482  om1r  7484  oe1m  7486  omword1  7514  omword2  7515  omlimcl  7519  oneo  7522  oewordi  7532  oelim2  7536  oeoa  7538  oeoe  7540  oeeui  7543  oaabs2  7586  endisj  7906  sdom1  8019  sucxpdom  8028  oancom  8405  cnfcom3lem  8457  pm54.43lem  8682  pm54.43  8683  infxpenc  8698  infxpenc2  8702  uncdadom  8850  cdaun  8851  cdaen  8852  cda1dif  8855  pm110.643  8856  pm110.643ALT  8857  cdacomen  8860  cdaassen  8861  xpcdaen  8862  mapcdaen  8863  cdaxpdom  8868  cdafi  8869  cdainf  8871  infcda1  8872  pwcda1  8873  pwcdadom  8895  cfsuc  8936  isfin4-3  8994  dcomex  9126  pwcfsdom  9258  pwxpndom2  9340  wunex2  9413  wuncval2  9422  tsk2  9440  sadcf  14956  sadcp1  14958  xpscg  15984  xpscfn  15985  xpsc0  15986  xpsc1  15987  xpsfrnel  15989  xpsfrnel2  15991  xpsle  16007  efgmnvl  17893  efgi1  17900  frgpuptinv  17950  frgpnabllem1  18042  dmdprdpr  18214  dprdpr  18215  psr1crng  19321  psr1assa  19322  psr1tos  19323  psr1bas  19325  vr1cl2  19327  ply1lss  19330  ply1subrg  19331  coe1fval3  19342  ressply1bas2  19362  ressply1add  19364  ressply1mul  19365  ressply1vsca  19366  subrgply1  19367  00ply1bas  19374  ply1plusgfvi  19376  psr1ring  19381  psr1lmod  19383  psr1sca  19384  ply1ascl  19392  subrg1ascl  19393  subrg1asclcl  19394  subrgvr1  19395  subrgvr1cl  19396  coe1z  19397  coe1mul2lem1  19401  coe1mul2  19403  coe1tm  19407  evls1val  19449  evls1rhm  19451  evls1sca  19452  evl1val  19457  evl1rhm  19460  evl1sca  19462  evl1var  19464  evls1var  19466  mpfpf1  19479  pf1mpf  19480  pf1ind  19483  xkofvcn  21236  xpstopnlem1  21361  xpstopnlem2  21363  ufildom1  21479  xpsdsval  21934  deg1z  23565  deg1addle  23579  deg1vscale  23582  deg1vsca  23583  deg1mulle2  23587  deg1le0  23589  ply1nzb  23600  sltval2  30856  nofv  30857  noxp1o  30866  sltsolem1  30870  bdayfo  30877  nobnddown  30903  rankeq1o  31251  ssoninhaus  31420  onint1  31421  finxp1o  32205  finxpreclem3  32206  finxpreclem4  32207  finxpreclem5  32208  finxpsuclem  32210  pw2f1ocnv  36422  wepwsolem  36430  pwfi2f1o  36484  clsk3nimkb  37158  clsk1indlem4  37162  clsk1indlem1  37163  ply1ass23l  41963
  Copyright terms: Public domain W3C validator