Theorem 1on 8462

Description: Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) Avoid ax-un 7730. (Revised by BTernaryTau, 30-Nov-2024.)

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8449	. 2 ⊢ 1o = suc ∅
2		0elon 6413	. . 3 ⊢ ∅ ∈ On
3		1oex 8459	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2866	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7804	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 704	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2865	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2149  Vcvv 3463  ∅c0 4294  Oncon0 6357  suc csuc 6359  1_oc1o 8442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-tr 5220  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6360  df-on 6361  df-suc 6363  df-1o 8449

This theorem is referenced by:  2on  8463  nlim2  8471  ord1eln01  8477  ondif2  8483  2oconcl  8484  fnoe  8491  oesuclem  8506  oecl  8518  o1p1e2  8521  om1r  8524  oe1m  8526  omword1  8554  omword2  8555  omlimcl  8559  oneo  8562  om2  8567  oewordi  8573  oelim2  8577  oeoa  8579  oeoe  8581  oeeui  8584  1onn  8622  oaabs2  8631  sucxpdom  9217  en2  9236  oancom  9616  cnfcom3lem  9668  ssttrcl  9680  ttrcltr  9681  dmttrcl  9686  ttrclselem2  9691  pm54.43lem  9982  pm54.43  9983  infxpenc  9998  infxpenc2  10002  undjudom  10147  endjudisj  10148  djuen  10149  dju1p1e2  10153  dju1p1e2ALT  10154  xpdjuen  10159  mapdjuen  10160  djuxpdom  10165  djufi  10166  djuinf  10168  infdju1  10169  pwdju1  10170  pwdjudom  10194  isfin4p1  10295  pwxpndom2  10646  wunex2  10719  wuncval2  10728  tsk2  10746  efgmnvl  19780  frgpnabllem1  19939  dmdprdpr  20117  dprdpr  20118  psr1crng  22312  psr1assa  22313  psr1tos  22314  psr1bas  22316  vr1cl2  22318  ply1lss  22321  ply1subrg  22322  ply1ass23l  22351  ressply1bas2  22352  ressply1add  22354  ressply1mul  22355  ressply1vsca  22356  subrgply1  22357  ply1plusgfvi  22366  psr1ring  22371  psr1lmod  22373  psr1sca  22374  ply1ascl  22384  subrg1ascl  22385  subrg1asclcl  22386  subrgvr1  22387  subrgvr1cl  22388  coe1z  22389  coe1mul2lem1  22393  coe1mul2  22395  coe1tm  22399  evls1val  22445  evls1rhm  22447  evls1sca  22448  evl1val  22454  evl1rhm  22457  evl1sca  22459  evl1var  22461  evls1var  22463  mpfpf1  22476  pf1mpf  22477  pf1ind  22480  xkofvcn  23806  xpstopnlem1  23931  ufildom1  24048  deg1z  26209  deg1addle  26223  deg1vscale  26226  deg1vsca  26227  deg1mulle2  26231  deg1le0  26233  ply1nzb  26245  ltsval2  27782  noextendlt  27795  ltssolem1  27801  nosepnelem  27805  nolt02o  27821  old1  28020  rankeq1o  36558  ssoninhaus  36844  onint1  36845  1oequni2o  37897  finxp1o  37921  finxpreclem3  37922  finxpreclem4  37923  finxpreclem5  37924  finxpsuclem  37926  pw2f1ocnv  43649  wepwsolem  43654  pwfi2f1o  43708  oaabsb  43906  oaordnr  43908  omnord1  43917  oege1  43918  oaomoencom  43929  omabs2  43944  omcl3g  43946  nadd1suc  44004  oe2  44017  safesnsupfiss  44026  safesnsupfidom1o  44028  safesnsupfilb  44029  1fno  44047  nlim2NEW  44054  oa1cl  44058  sn1dom  44137  pr2dom  44138  tr3dom  44139  clsk1indlem4  44655  setc1onsubc  50258