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

Theorem 1on 7719
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 7712 . 2 1𝑜 = suc ∅
2 0elon 5921 . . 3 ∅ ∈ On
32onsuci 7184 . 2 suc ∅ ∈ On
41, 3eqeltri 2845 1 1𝑜 ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 2144  c0 4061  Oncon0 5866  suc csuc 5868  1𝑜c1o 7705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pr 5034  ax-un 7095
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-br 4785  df-opab 4845  df-tr 4885  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-ord 5869  df-on 5870  df-suc 5872  df-1o 7712
This theorem is referenced by:  1oex  7720  2on  7721  ondif2  7735  2oconcl  7736  fnoe  7743  oesuclem  7758  oecl  7770  o1p1e2  7773  o2p2e4  7774  om1r  7776  oe1m  7778  omword1  7806  omword2  7807  omlimcl  7811  oneo  7814  oewordi  7824  oelim2  7828  oeoa  7830  oeoe  7832  oeeui  7835  oaabs2  7878  sucxpdom  8324  oancom  8711  cnfcom3lem  8763  pm54.43lem  9024  pm54.43  9025  infxpenc  9040  infxpenc2  9044  uncdadom  9194  cdaun  9195  cdaen  9196  cda1dif  9199  pm110.643  9200  pm110.643ALT  9201  cdacomen  9204  cdaassen  9205  xpcdaen  9206  mapcdaen  9207  cdaxpdom  9212  cdafi  9213  cdainf  9215  infcda1  9216  pwcda1  9217  pwcdadom  9239  isfin4-3  9338  pwxpndom2  9688  wunex2  9761  wuncval2  9770  tsk2  9788  xpscg  16425  xpscfn  16426  xpsc1  16428  efgmnvl  18333  frgpnabllem1  18482  dmdprdpr  18655  dprdpr  18656  psr1crng  19771  psr1assa  19772  psr1tos  19773  psr1bas  19775  vr1cl2  19777  ply1lss  19780  ply1subrg  19781  ressply1bas2  19812  ressply1add  19814  ressply1mul  19815  ressply1vsca  19816  subrgply1  19817  ply1plusgfvi  19826  psr1ring  19831  psr1lmod  19833  psr1sca  19834  ply1ascl  19842  subrg1ascl  19843  subrg1asclcl  19844  subrgvr1  19845  subrgvr1cl  19846  coe1z  19847  coe1mul2lem1  19851  coe1mul2  19853  coe1tm  19857  evls1val  19899  evls1rhm  19901  evls1sca  19902  evl1val  19907  evl1rhm  19910  evl1sca  19912  evl1var  19914  evls1var  19916  mpfpf1  19929  pf1mpf  19930  pf1ind  19933  xkofvcn  21707  xpstopnlem1  21832  ufildom1  21949  deg1z  24066  deg1addle  24080  deg1vscale  24083  deg1vsca  24084  deg1mulle2  24088  deg1le0  24090  ply1nzb  24101  sltval2  32140  noextendlt  32153  sltsolem1  32157  nosepnelem  32161  nolt02o  32176  rankeq1o  32609  ssoninhaus  32778  onint1  32779  1oequni2o  33546  finxp1o  33559  finxpreclem3  33560  finxpreclem4  33561  finxpreclem5  33562  finxpsuclem  33564  pw2f1ocnv  38123  wepwsolem  38131  pwfi2f1o  38185  clsk1indlem4  38861  ply1ass23l  42688
  Copyright terms: Public domain W3C validator