Theorem 1on 8449

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8437	. 2 ⊢ 1o = suc ∅
2		0elon 6390	. . 3 ⊢ ∅ ∈ On
3		1oex 8447	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2826	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7788	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2825	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2109  Vcvv 3450  ∅c0 4299  Oncon0 6335  suc csuc 6337  1_oc1o 8430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339  df-suc 6341  df-1o 8437

This theorem is referenced by:  2on  8450  nlim2  8457  ord1eln01  8463  ondif2  8469  2oconcl  8470  fnoe  8477  oesuclem  8492  oecl  8504  o1p1e2  8507  om1r  8510  oe1m  8512  omword1  8540  omword2  8541  omlimcl  8545  oneo  8548  oewordi  8558  oelim2  8562  oeoa  8564  oeoe  8566  oeeui  8569  1onn  8607  oaabs2  8616  enpr2dOLD  9024  sucxpdom  9209  en2  9233  oancom  9611  cnfcom3lem  9663  ssttrcl  9675  ttrcltr  9676  dmttrcl  9681  ttrclselem2  9686  pm54.43lem  9960  pm54.43  9961  infxpenc  9978  infxpenc2  9982  undjudom  10128  endjudisj  10129  djuen  10130  dju1p1e2  10134  dju1p1e2ALT  10135  xpdjuen  10140  mapdjuen  10141  djuxpdom  10146  djufi  10147  djuinf  10149  infdju1  10150  pwdju1  10151  pwdjudom  10175  isfin4p1  10275  pwxpndom2  10625  wunex2  10698  wuncval2  10707  tsk2  10725  efgmnvl  19651  frgpnabllem1  19810  dmdprdpr  19988  dprdpr  19989  psr1crng  22078  psr1assa  22079  psr1tos  22080  psr1bas  22082  vr1cl2  22084  ply1lss  22088  ply1subrg  22089  ply1ass23l  22118  ressply1bas2  22119  ressply1add  22121  ressply1mul  22122  ressply1vsca  22123  subrgply1  22124  ply1plusgfvi  22133  psr1ring  22138  psr1lmod  22140  psr1sca  22141  ply1ascl  22151  subrg1ascl  22152  subrg1asclcl  22153  subrgvr1  22154  subrgvr1cl  22155  coe1z  22156  coe1mul2lem1  22160  coe1mul2  22162  coe1tm  22166  evls1val  22214  evls1rhm  22216  evls1sca  22217  evl1val  22223  evl1rhm  22226  evl1sca  22228  evl1var  22230  evls1var  22232  mpfpf1  22245  pf1mpf  22246  pf1ind  22249  xkofvcn  23578  xpstopnlem1  23703  ufildom1  23820  deg1z  25999  deg1addle  26013  deg1vscale  26016  deg1vsca  26017  deg1mulle2  26021  deg1le0  26023  ply1nzb  26035  sltval2  27575  noextendlt  27588  sltsolem1  27594  nosepnelem  27598  nolt02o  27614  old1  27794  rankeq1o  36166  ssoninhaus  36443  onint1  36444  1oequni2o  37363  finxp1o  37387  finxpreclem3  37388  finxpreclem4  37389  finxpreclem5  37390  finxpsuclem  37392  pw2f1ocnv  43033  wepwsolem  43038  pwfi2f1o  43092  oaabsb  43290  oaordnr  43292  omnord1  43301  oege1  43302  oaomoencom  43313  omabs2  43328  omcl3g  43330  nadd1suc  43388  om2  43400  oe2  43402  safesnsupfiss  43411  safesnsupfidom1o  43413  safesnsupfilb  43414  1no  43432  nlim2NEW  43439  oa1cl  43443  sn1dom  43522  pr2dom  43523  tr3dom  43524  clsk1indlem4  44040