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

Theorem 1on 7552
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 7545 . 2 1𝑜 = suc ∅
2 0elon 5766 . . 3 ∅ ∈ On
32onsuci 7023 . 2 suc ∅ ∈ On
41, 3eqeltri 2695 1 1𝑜 ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 1988  c0 3907  Oncon0 5711  suc csuc 5713  1𝑜c1o 7538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-tr 4744  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-ord 5714  df-on 5715  df-suc 5717  df-1o 7545
This theorem is referenced by:  2on  7553  ondif2  7567  2oconcl  7568  fnoe  7575  oev  7579  oe0  7587  oev2  7588  oesuclem  7590  oecl  7602  o1p1e2  7605  o2p2e4  7606  om1r  7608  oe1m  7610  omword1  7638  omword2  7639  omlimcl  7643  oneo  7646  oewordi  7656  oelim2  7660  oeoa  7662  oeoe  7664  oeeui  7667  oaabs2  7710  endisj  8032  sdom1  8145  sucxpdom  8154  oancom  8533  cnfcom3lem  8585  pm54.43lem  8810  pm54.43  8811  infxpenc  8826  infxpenc2  8830  uncdadom  8978  cdaun  8979  cdaen  8980  cda1dif  8983  pm110.643  8984  pm110.643ALT  8985  cdacomen  8988  cdaassen  8989  xpcdaen  8990  mapcdaen  8991  cdaxpdom  8996  cdafi  8997  cdainf  8999  infcda1  9000  pwcda1  9001  pwcdadom  9023  cfsuc  9064  isfin4-3  9122  dcomex  9254  pwcfsdom  9390  pwxpndom2  9472  wunex2  9545  wuncval2  9554  tsk2  9572  sadcf  15156  sadcp1  15158  xpscg  16199  xpscfn  16200  xpsc0  16201  xpsc1  16202  xpsfrnel  16204  xpsfrnel2  16206  xpsle  16222  efgmnvl  18108  efgi1  18115  frgpuptinv  18165  frgpnabllem1  18257  dmdprdpr  18429  dprdpr  18430  psr1crng  19538  psr1assa  19539  psr1tos  19540  psr1bas  19542  vr1cl2  19544  ply1lss  19547  ply1subrg  19548  coe1fval3  19559  ressply1bas2  19579  ressply1add  19581  ressply1mul  19582  ressply1vsca  19583  subrgply1  19584  00ply1bas  19591  ply1plusgfvi  19593  psr1ring  19598  psr1lmod  19600  psr1sca  19601  ply1ascl  19609  subrg1ascl  19610  subrg1asclcl  19611  subrgvr1  19612  subrgvr1cl  19613  coe1z  19614  coe1mul2lem1  19618  coe1mul2  19620  coe1tm  19624  evls1val  19666  evls1rhm  19668  evls1sca  19669  evl1val  19674  evl1rhm  19677  evl1sca  19679  evl1var  19681  evls1var  19683  mpfpf1  19696  pf1mpf  19697  pf1ind  19700  xkofvcn  21468  xpstopnlem1  21593  xpstopnlem2  21595  ufildom1  21711  xpsdsval  22167  deg1z  23828  deg1addle  23842  deg1vscale  23845  deg1vsca  23846  deg1mulle2  23850  deg1le0  23852  ply1nzb  23863  sltval2  31783  nofv  31784  noxp1o  31790  noextendlt  31796  sltsolem1  31800  bdayfo  31802  nosepnelem  31804  nosep1o  31806  nosepdmlem  31807  nolt02o  31819  nosupbnd1lem5  31832  nosupbnd2lem1  31835  noetalem1  31837  noetalem3  31839  noetalem4  31840  rankeq1o  32253  ssoninhaus  32422  onint1  32423  finxp1o  33200  finxpreclem3  33201  finxpreclem4  33202  finxpreclem5  33203  finxpsuclem  33205  pw2f1ocnv  37423  wepwsolem  37431  pwfi2f1o  37485  clsk3nimkb  38158  clsk1indlem4  38162  clsk1indlem1  38163  ply1ass23l  41935
  Copyright terms: Public domain W3C validator