Theorem 1on 8419

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8407	. 2 ⊢ 1o = suc ∅
2		0elon 6380	. . 3 ⊢ ∅ ∈ On
3		1oex 8417	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2834	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7764	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 693	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2833	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ∅c0 4287  Oncon0 6325  suc csuc 6327  1_oc1o 8400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-on 6329  df-suc 6331  df-1o 8407

This theorem is referenced by:  2on  8420  nlim2  8427  ord1eln01  8433  ondif2  8439  2oconcl  8440  fnoe  8447  oesuclem  8462  oecl  8474  o1p1e2  8477  om1r  8480  oe1m  8482  omword1  8510  omword2  8511  omlimcl  8515  oneo  8518  om2  8523  oewordi  8529  oelim2  8533  oeoa  8535  oeoe  8537  oeeui  8540  1onn  8578  oaabs2  8587  sucxpdom  9173  en2  9192  oancom  9572  cnfcom3lem  9624  ssttrcl  9636  ttrcltr  9637  dmttrcl  9642  ttrclselem2  9647  pm54.43lem  9924  pm54.43  9925  infxpenc  9940  infxpenc2  9944  undjudom  10090  endjudisj  10091  djuen  10092  dju1p1e2  10096  dju1p1e2ALT  10097  xpdjuen  10102  mapdjuen  10103  djuxpdom  10108  djufi  10109  djuinf  10111  infdju1  10112  pwdju1  10113  pwdjudom  10137  isfin4p1  10237  pwxpndom2  10588  wunex2  10661  wuncval2  10670  tsk2  10688  efgmnvl  19655  frgpnabllem1  19814  dmdprdpr  19992  dprdpr  19993  psr1crng  22139  psr1assa  22140  psr1tos  22141  psr1bas  22143  vr1cl2  22145  ply1lss  22149  ply1subrg  22150  ply1ass23l  22179  ressply1bas2  22180  ressply1add  22182  ressply1mul  22183  ressply1vsca  22184  subrgply1  22185  ply1plusgfvi  22194  psr1ring  22199  psr1lmod  22201  psr1sca  22202  ply1ascl  22212  subrg1ascl  22213  subrg1asclcl  22214  subrgvr1  22215  subrgvr1cl  22216  coe1z  22217  coe1mul2lem1  22221  coe1mul2  22223  coe1tm  22227  evls1val  22276  evls1rhm  22278  evls1sca  22279  evl1val  22285  evl1rhm  22288  evl1sca  22290  evl1var  22292  evls1var  22294  mpfpf1  22307  pf1mpf  22308  pf1ind  22311  xkofvcn  23640  xpstopnlem1  23765  ufildom1  23882  deg1z  26060  deg1addle  26074  deg1vscale  26077  deg1vsca  26078  deg1mulle2  26082  deg1le0  26084  ply1nzb  26096  ltsval2  27636  noextendlt  27649  ltssolem1  27655  nosepnelem  27659  nolt02o  27675  old1  27873  rankeq1o  36384  ssoninhaus  36661  onint1  36662  1oequni2o  37620  finxp1o  37644  finxpreclem3  37645  finxpreclem4  37646  finxpreclem5  37647  finxpsuclem  37649  pw2f1ocnv  43391  wepwsolem  43396  pwfi2f1o  43450  oaabsb  43648  oaordnr  43650  omnord1  43659  oege1  43660  oaomoencom  43671  omabs2  43686  omcl3g  43688  nadd1suc  43746  oe2  43759  safesnsupfiss  43768  safesnsupfidom1o  43770  safesnsupfilb  43771  1fno  43789  nlim2NEW  43796  oa1cl  43800  sn1dom  43879  pr2dom  43880  tr3dom  43881  clsk1indlem4  44397