Theorem 1on 7567

Description: Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.)

Assertion

Ref	Expression
1on	|- 1o e. On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 7560	. 2 |- 1o = suc (/)
2		0elon 5778	. . 3 |- (/) e. On
3	2	onsuci 7038	. 2 |- suc (/) e. On
4	1, 3	eqeltri 2697	1 |- 1o e. On

Syntax hints:   e. wcel 1990   (/)c0 3915   Oncon0 5723   suc csuc 5725   1oc1o 7553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-tr 4753  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-ord 5726  df-on 5727  df-suc 5729  df-1o 7560

This theorem is referenced by:  2on  7568  ondif2  7582  2oconcl  7583  fnoe  7590  oev  7594  oe0  7602  oev2  7603  oesuclem  7605  oecl  7617  o1p1e2  7620  o2p2e4  7621  om1r  7623  oe1m  7625  omword1  7653  omword2  7654  omlimcl  7658  oneo  7661  oewordi  7671  oelim2  7675  oeoa  7677  oeoe  7679  oeeui  7682  oaabs2  7725  endisj  8047  sdom1  8160  sucxpdom  8169  oancom  8548  cnfcom3lem  8600  pm54.43lem  8825  pm54.43  8826  infxpenc  8841  infxpenc2  8845  uncdadom  8993  cdaun  8994  cdaen  8995  cda1dif  8998  pm110.643  8999  pm110.643ALT  9000  cdacomen  9003  cdaassen  9004  xpcdaen  9005  mapcdaen  9006  cdaxpdom  9011  cdafi  9012  cdainf  9014  infcda1  9015  pwcda1  9016  pwcdadom  9038  cfsuc  9079  isfin4-3  9137  dcomex  9269  pwcfsdom  9405  pwxpndom2  9487  wunex2  9560  wuncval2  9569  tsk2  9587  sadcf  15175  sadcp1  15177  xpscg  16218  xpscfn  16219  xpsc0  16220  xpsc1  16221  xpsfrnel  16223  xpsfrnel2  16225  xpsle  16241  efgmnvl  18127  efgi1  18134  frgpuptinv  18184  frgpnabllem1  18276  dmdprdpr  18448  dprdpr  18449  psr1crng  19557  psr1assa  19558  psr1tos  19559  psr1bas  19561  vr1cl2  19563  ply1lss  19566  ply1subrg  19567  coe1fval3  19578  ressply1bas2  19598  ressply1add  19600  ressply1mul  19601  ressply1vsca  19602  subrgply1  19603  00ply1bas  19610  ply1plusgfvi  19612  psr1ring  19617  psr1lmod  19619  psr1sca  19620  ply1ascl  19628  subrg1ascl  19629  subrg1asclcl  19630  subrgvr1  19631  subrgvr1cl  19632  coe1z  19633  coe1mul2lem1  19637  coe1mul2  19639  coe1tm  19643  evls1val  19685  evls1rhm  19687  evls1sca  19688  evl1val  19693  evl1rhm  19696  evl1sca  19698  evl1var  19700  evls1var  19702  mpfpf1  19715  pf1mpf  19716  pf1ind  19719  xkofvcn  21487  xpstopnlem1  21612  xpstopnlem2  21614  ufildom1  21730  xpsdsval  22186  deg1z  23847  deg1addle  23861  deg1vscale  23864  deg1vsca  23865  deg1mulle2  23869  deg1le0  23871  ply1nzb  23882  sltval2  31809  nofv  31810  noxp1o  31816  noextendlt  31822  sltsolem1  31826  bdayfo  31828  nosepnelem  31830  nosep1o  31832  nosepdmlem  31833  nolt02o  31845  nosupbnd1lem5  31858  nosupbnd2lem1  31861  noetalem1  31863  noetalem3  31865  noetalem4  31866  rankeq1o  32278  ssoninhaus  32447  onint1  32448  finxp1o  33229  finxpreclem3  33230  finxpreclem4  33231  finxpreclem5  33232  finxpsuclem  33234  pw2f1ocnv  37604  wepwsolem  37612  pwfi2f1o  37666  clsk3nimkb  38338  clsk1indlem4  38342  clsk1indlem1  38343  ply1ass23l  42170