Theorem 1on 8409

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8397	. 2 ⊢ 1o = suc ∅
2		0elon 6372	. . 3 ⊢ ∅ ∈ On
3		1oex 8407	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2833	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7754	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2832	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2113  Vcvv 3440  ∅c0 4285  Oncon0 6317  suc csuc 6319  1_oc1o 8390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-tr 5206  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-suc 6323  df-1o 8397

This theorem is referenced by:  2on  8410  nlim2  8417  ord1eln01  8423  ondif2  8429  2oconcl  8430  fnoe  8437  oesuclem  8452  oecl  8464  o1p1e2  8467  om1r  8470  oe1m  8472  omword1  8500  omword2  8501  omlimcl  8505  oneo  8508  om2  8513  oewordi  8519  oelim2  8523  oeoa  8525  oeoe  8527  oeeui  8530  1onn  8568  oaabs2  8577  sucxpdom  9161  en2  9180  oancom  9560  cnfcom3lem  9612  ssttrcl  9624  ttrcltr  9625  dmttrcl  9630  ttrclselem2  9635  pm54.43lem  9912  pm54.43  9913  infxpenc  9928  infxpenc2  9932  undjudom  10078  endjudisj  10079  djuen  10080  dju1p1e2  10084  dju1p1e2ALT  10085  xpdjuen  10090  mapdjuen  10091  djuxpdom  10096  djufi  10097  djuinf  10099  infdju1  10100  pwdju1  10101  pwdjudom  10125  isfin4p1  10225  pwxpndom2  10576  wunex2  10649  wuncval2  10658  tsk2  10676  efgmnvl  19643  frgpnabllem1  19802  dmdprdpr  19980  dprdpr  19981  psr1crng  22127  psr1assa  22128  psr1tos  22129  psr1bas  22131  vr1cl2  22133  ply1lss  22137  ply1subrg  22138  ply1ass23l  22167  ressply1bas2  22168  ressply1add  22170  ressply1mul  22171  ressply1vsca  22172  subrgply1  22173  ply1plusgfvi  22182  psr1ring  22187  psr1lmod  22189  psr1sca  22190  ply1ascl  22200  subrg1ascl  22201  subrg1asclcl  22202  subrgvr1  22203  subrgvr1cl  22204  coe1z  22205  coe1mul2lem1  22209  coe1mul2  22211  coe1tm  22215  evls1val  22264  evls1rhm  22266  evls1sca  22267  evl1val  22273  evl1rhm  22276  evl1sca  22278  evl1var  22280  evls1var  22282  mpfpf1  22295  pf1mpf  22296  pf1ind  22299  xkofvcn  23628  xpstopnlem1  23753  ufildom1  23870  deg1z  26048  deg1addle  26062  deg1vscale  26065  deg1vsca  26066  deg1mulle2  26070  deg1le0  26072  ply1nzb  26084  ltsval2  27624  noextendlt  27637  ltssolem1  27643  nosepnelem  27647  nolt02o  27663  old1  27861  rankeq1o  36365  ssoninhaus  36642  onint1  36643  1oequni2o  37573  finxp1o  37597  finxpreclem3  37598  finxpreclem4  37599  finxpreclem5  37600  finxpsuclem  37602  pw2f1ocnv  43279  wepwsolem  43284  pwfi2f1o  43338  oaabsb  43536  oaordnr  43538  omnord1  43547  oege1  43548  oaomoencom  43559  omabs2  43574  omcl3g  43576  nadd1suc  43634  oe2  43647  safesnsupfiss  43656  safesnsupfidom1o  43658  safesnsupfilb  43659  1fno  43677  nlim2NEW  43684  oa1cl  43688  sn1dom  43767  pr2dom  43768  tr3dom  43769  clsk1indlem4  44285