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

Theorem 1on 7195
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 7188 . 2  |-  1o  =  suc  (/)
2 0elon 5493 . . 3  |-  (/)  e.  On
32onsuci 6677 . 2  |-  suc  (/)  e.  On
41, 3eqeltri 2507 1  |-  1o  e.  On
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1869   (/)c0 3762   Oncon0 5440   suc csuc 5442   1oc1o 7181
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658  ax-un 6595
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-tr 4517  df-eprel 4762  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-ord 5443  df-on 5444  df-suc 5446  df-1o 7188
This theorem is referenced by:  2on  7196  ondif2  7210  2oconcl  7211  fnoe  7218  oev  7222  oe0  7230  oev2  7231  oesuclem  7233  oecl  7245  o1p1e2  7248  om1r  7250  oe1m  7252  omword1  7280  omword2  7281  omlimcl  7285  oneo  7288  oewordi  7298  oelim2  7302  oeoa  7304  oeoe  7306  oeeui  7309  oaabs2  7352  endisj  7663  sdom1  7776  sucxpdom  7785  oancom  8160  cnfcom3lem  8211  pm54.43lem  8436  pm54.43  8437  infxpenc  8451  infxpenc2  8455  uncdadom  8603  cdaun  8604  cdaen  8605  cda1dif  8608  pm110.643  8609  pm110.643ALT  8610  cdacomen  8613  cdaassen  8614  xpcdaen  8615  mapcdaen  8616  cdaxpdom  8621  cdafi  8622  cdainf  8624  infcda1  8625  pwcda1  8626  pwcdadom  8648  cfsuc  8689  isfin4-3  8747  dcomex  8879  pwcfsdom  9010  pwxpndom2  9092  wunex2  9165  wuncval2  9174  tsk2  9192  sadcf  14420  sadcp1  14422  xpscg  15457  xpscfn  15458  xpsc0  15459  xpsc1  15460  xpsfrnel  15462  xpsfrnel2  15464  xpsle  15480  efgmnvl  17357  efgi1  17364  frgpuptinv  17414  frgpnabllem1  17502  dmdprdpr  17675  dprdpr  17676  psr1crng  18773  psr1assa  18774  psr1tos  18775  psr1bas  18777  vr1cl2  18779  ply1lss  18782  ply1subrg  18783  coe1fval3  18794  ressply1bas2  18814  ressply1add  18816  ressply1mul  18817  ressply1vsca  18818  subrgply1  18819  00ply1bas  18826  ply1plusgfvi  18828  psr1ring  18833  psr1lmod  18835  psr1sca  18836  ply1ascl  18844  subrg1ascl  18845  subrg1asclcl  18846  subrgvr1  18847  subrgvr1cl  18848  coe1z  18849  coe1mul2lem1  18853  coe1mul2  18855  coe1tm  18859  evls1val  18902  evls1rhm  18904  evls1sca  18905  evl1val  18910  evl1rhm  18913  evl1sca  18915  evl1var  18917  evls1var  18919  mpfpf1  18932  pf1mpf  18933  pf1ind  18936  xkofvcn  20691  xpstopnlem1  20816  xpstopnlem2  20818  ufildom1  20933  xpsdsval  21388  deg1z  23028  deg1addle  23042  deg1vscale  23045  deg1vsca  23046  deg1mulle2  23050  deg1le0  23052  ply1nzb  23063  sltval2  30544  nofv  30545  noxp1o  30554  sltsolem1  30556  bdayfo  30563  nobnddown  30589  rankeq1o  30937  ssoninhaus  31107  onint1  31108  finxp1o  31742  finxpreclem3  31743  finxpreclem4  31744  finxpreclem5  31745  finxpsuclem  31747  pw2f1ocnv  35856  wepwsolem  35864  pwfi2f1o  35918  ply1ass23l  39518
  Copyright terms: Public domain W3C validator