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

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

Proof of Theorem 1on
StepHypRef Expression
1 df-1o 6716 . 2  |-  1o  =  suc  (/)
2 0elon 4626 . . 3  |-  (/)  e.  On
32onsuci 4810 . 2  |-  suc  (/)  e.  On
41, 3eqeltri 2505 1  |-  1o  e.  On
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   (/)c0 3620   Oncon0 4573   suc csuc 4575   1oc1o 6709
This theorem is referenced by:  2on  6724  ondif2  6738  2oconcl  6739  fnoe  6746  oev  6750  oe0  6758  oev2  6759  oesuclem  6761  oecl  6773  o1p1e2  6776  om1r  6778  oe1m  6780  omword1  6808  omword2  6809  omlimcl  6813  oneo  6816  oewordi  6826  oelim2  6830  oeoa  6832  oeoe  6834  oeeui  6837  oaabs2  6880  endisj  7187  sdom1  7300  sucxpdom  7310  oancom  7598  cnfcom3lem  7652  pm54.43lem  7878  pm54.43  7879  infxpenc  7891  infxpenc2  7895  uncdadom  8043  cdaun  8044  cdaen  8045  cda1dif  8048  pm110.643  8049  pm110.643ALT  8050  cdacomen  8053  cdaassen  8054  xpcdaen  8055  mapcdaen  8056  cdaxpdom  8061  cdafi  8062  cdainf  8064  infcda1  8065  pwcda1  8066  pwcdadom  8088  cfsuc  8129  isfin4-3  8187  dcomex  8319  pwcfsdom  8450  pwxpndom2  8532  wunex2  8605  wuncval2  8614  tsk2  8632  sadcf  12957  sadcp1  12959  xpscg  13775  xpscfn  13776  xpsc0  13777  xpsc1  13778  xpsfrnel  13780  xpsfrnel2  13782  xpsle  13798  efgmnvl  15338  efgi1  15345  frgpuptinv  15395  frgpnabllem1  15476  dmdprdpr  15599  dprdpr  15600  psr1crng  16577  psr1assa  16578  psr1tos  16579  psr1bas  16581  vr1cl2  16583  ply1lss  16586  ply1subrg  16587  coe1fval3  16598  ressply1bas2  16614  ressply1add  16616  ressply1mul  16617  ressply1vsca  16618  subrgply1  16619  00ply1bas  16626  ply1plusgfvi  16628  psr1rng  16633  psr1lmod  16635  psr1sca  16636  ply1ascl  16643  subrg1ascl  16644  subrg1asclcl  16645  subrgvr1  16646  subrgvr1cl  16647  coe1z  16648  coe1mul2lem1  16652  coe1mul2  16654  coe1tm  16657  xkofvcn  17708  xpstopnlem1  17833  xpstopnlem2  17835  ufildom1  17950  xpsdsval  18403  evl1val  19940  evl1rhm  19941  evl1sca  19942  evl1var  19944  mpfpf1  19963  pf1mpf  19964  pf1ind  19967  deg1z  20002  deg1addle  20016  deg1vscale  20019  deg1vsca  20020  deg1mulle2  20024  deg1le0  20026  ply1nzb  20037  sltval2  25603  nofv  25604  noxp1o  25613  sltsolem1  25615  bdayfo  25622  nobnddown  25648  rankeq1o  26104  ssoninhaus  26190  onint1  26191  pw2f1ocnv  27089  wepwsolem  27097  pwfi2f1o  27218
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395  ax-un 4693
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-tr 4295  df-eprel 4486  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-suc 4579  df-1o 6716
  Copyright terms: Public domain W3C validator