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

Theorem 1on 6486
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 6479 . 2  |-  1o  =  suc  (/)
2 0elon 4445 . . 3  |-  (/)  e.  On
32onsuci 4629 . 2  |-  suc  (/)  e.  On
41, 3eqeltri 2353 1  |-  1o  e.  On
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   (/)c0 3455   Oncon0 4392   suc csuc 4394   1oc1o 6472
This theorem is referenced by:  2on  6487  ondif2  6501  2oconcl  6502  fnoe  6509  oev  6513  oe0  6521  oev2  6522  oesuclem  6524  oecl  6536  o1p1e2  6539  om1r  6541  oe1m  6543  omword1  6571  omword2  6572  omlimcl  6576  oneo  6579  oewordi  6589  oelim2  6593  oeoa  6595  oeoe  6597  oeeui  6600  oaabs2  6643  endisj  6949  sdom1  7062  sucxpdom  7072  oancom  7352  cnfcom3lem  7406  pm54.43lem  7632  pm54.43  7633  infxpenc  7645  infxpenc2  7649  uncdadom  7797  cdaun  7798  cdaen  7799  cda1dif  7802  pm110.643  7803  pm110.643ALT  7804  cdacomen  7807  cdaassen  7808  xpcdaen  7809  mapcdaen  7810  cdaxpdom  7815  cdafi  7816  cdainf  7818  infcda1  7819  pwcda1  7820  pwcdadom  7842  cfsuc  7883  isfin4-3  7941  dcomex  8073  pwcfsdom  8205  pwxpndom2  8287  wunex2  8360  wuncval2  8369  tsk2  8387  sadcf  12644  sadcp1  12646  xpscg  13460  xpscfn  13461  xpsc0  13462  xpsc1  13463  xpsfrnel  13465  xpsfrnel2  13467  xpsle  13483  efgmnvl  15023  efgi1  15030  frgpuptinv  15080  frgpnabllem1  15161  dmdprdpr  15284  dprdpr  15285  psr1crng  16266  psr1assa  16267  psr1tos  16268  psr1bas  16270  vr1cl2  16272  ply1lss  16275  ply1subrg  16276  coe1fval3  16289  ressply1bas2  16306  ressply1add  16308  ressply1mul  16309  ressply1vsca  16310  subrgply1  16311  00ply1bas  16318  ply1plusgfvi  16320  psr1rng  16325  psr1lmod  16327  psr1sca  16328  ply1ascl  16335  subrg1ascl  16336  subrg1asclcl  16337  subrgvr1  16338  subrgvr1cl  16339  coe1z  16340  coe1mul2lem1  16344  coe1mul2  16346  coe1tm  16349  xkofvcn  17378  xpstopnlem1  17500  xpstopnlem2  17502  ufildom1  17621  xpsdsval  17945  evl1val  19411  evl1rhm  19412  evl1sca  19413  evl1var  19415  mpfpf1  19434  pf1mpf  19435  pf1ind  19438  deg1z  19473  deg1addle  19487  deg1vscale  19490  deg1vsca  19491  deg1mulle2  19495  deg1le0  19497  ply1nzb  19508  sltval2  24310  nofv  24311  noxp1o  24320  sltsolem1  24322  bdayfo  24329  nobnddown  24355  rankeq1o  24801  ssoninhaus  24887  onint1  24888  pw2f1ocnv  27130  wepwsolem  27138  pwfi2f1o  27260
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-tr 4114  df-eprel 4305  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-suc 4398  df-1o 6479
  Copyright terms: Public domain W3C validator