Theorem 1on 8410

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8398	. 2 ⊢ 1o = suc ∅
2		0elon 6372	. . 3 ⊢ ∅ ∈ On
3		1oex 8408	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2834	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7756	. . 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 3430  ∅c0 4274  Oncon0 6317  suc csuc 6319  1_oc1o 8391

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 5231  ax-nul 5241  ax-pr 5370

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  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 8398

This theorem is referenced by:  2on  8411  nlim2  8418  ord1eln01  8424  ondif2  8430  2oconcl  8431  fnoe  8438  oesuclem  8453  oecl  8465  o1p1e2  8468  om1r  8471  oe1m  8473  omword1  8501  omword2  8502  omlimcl  8506  oneo  8509  om2  8514  oewordi  8520  oelim2  8524  oeoa  8526  oeoe  8528  oeeui  8531  1onn  8569  oaabs2  8578  sucxpdom  9164  en2  9183  oancom  9563  cnfcom3lem  9615  ssttrcl  9627  ttrcltr  9628  dmttrcl  9633  ttrclselem2  9638  pm54.43lem  9915  pm54.43  9916  infxpenc  9931  infxpenc2  9935  undjudom  10081  endjudisj  10082  djuen  10083  dju1p1e2  10087  dju1p1e2ALT  10088  xpdjuen  10093  mapdjuen  10094  djuxpdom  10099  djufi  10100  djuinf  10102  infdju1  10103  pwdju1  10104  pwdjudom  10128  isfin4p1  10228  pwxpndom2  10579  wunex2  10652  wuncval2  10661  tsk2  10679  efgmnvl  19680  frgpnabllem1  19839  dmdprdpr  20017  dprdpr  20018  psr1crng  22160  psr1assa  22161  psr1tos  22162  psr1bas  22164  vr1cl2  22166  ply1lss  22170  ply1subrg  22171  ply1ass23l  22200  ressply1bas2  22201  ressply1add  22203  ressply1mul  22204  ressply1vsca  22205  subrgply1  22206  ply1plusgfvi  22215  psr1ring  22220  psr1lmod  22222  psr1sca  22223  ply1ascl  22233  subrg1ascl  22234  subrg1asclcl  22235  subrgvr1  22236  subrgvr1cl  22237  coe1z  22238  coe1mul2lem1  22242  coe1mul2  22244  coe1tm  22248  evls1val  22295  evls1rhm  22297  evls1sca  22298  evl1val  22304  evl1rhm  22307  evl1sca  22309  evl1var  22311  evls1var  22313  mpfpf1  22326  pf1mpf  22327  pf1ind  22330  xkofvcn  23659  xpstopnlem1  23784  ufildom1  23901  deg1z  26062  deg1addle  26076  deg1vscale  26079  deg1vsca  26080  deg1mulle2  26084  deg1le0  26086  ply1nzb  26098  ltsval2  27634  noextendlt  27647  ltssolem1  27653  nosepnelem  27657  nolt02o  27673  old1  27871  rankeq1o  36369  ssoninhaus  36646  onint1  36647  1oequni2o  37698  finxp1o  37722  finxpreclem3  37723  finxpreclem4  37724  finxpreclem5  37725  finxpsuclem  37727  pw2f1ocnv  43483  wepwsolem  43488  pwfi2f1o  43542  oaabsb  43740  oaordnr  43742  omnord1  43751  oege1  43752  oaomoencom  43763  omabs2  43778  omcl3g  43780  nadd1suc  43838  oe2  43851  safesnsupfiss  43860  safesnsupfidom1o  43862  safesnsupfilb  43863  1fno  43881  nlim2NEW  43888  oa1cl  43892  sn1dom  43971  pr2dom  43972  tr3dom  43973  clsk1indlem4  44489