Theorem 1on 8407

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8395	. 2 ⊢ 1o = suc ∅
2		0elon 6366	. . 3 ⊢ ∅ ∈ On
3		1oex 8405	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2825	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7749	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2824	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2109  Vcvv 3438  ∅c0 4286  Oncon0 6311  suc csuc 6313  1_oc1o 8388

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 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-ord 6314  df-on 6315  df-suc 6317  df-1o 8395

This theorem is referenced by:  2on  8408  nlim2  8415  ord1eln01  8421  ondif2  8427  2oconcl  8428  fnoe  8435  oesuclem  8450  oecl  8462  o1p1e2  8465  om1r  8468  oe1m  8470  omword1  8498  omword2  8499  omlimcl  8503  oneo  8506  oewordi  8516  oelim2  8520  oeoa  8522  oeoe  8524  oeeui  8527  1onn  8565  oaabs2  8574  sucxpdom  9160  en2  9184  oancom  9566  cnfcom3lem  9618  ssttrcl  9630  ttrcltr  9631  dmttrcl  9636  ttrclselem2  9641  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  10578  wunex2  10651  wuncval2  10660  tsk2  10678  efgmnvl  19611  frgpnabllem1  19770  dmdprdpr  19948  dprdpr  19949  psr1crng  22087  psr1assa  22088  psr1tos  22089  psr1bas  22091  vr1cl2  22093  ply1lss  22097  ply1subrg  22098  ply1ass23l  22127  ressply1bas2  22128  ressply1add  22130  ressply1mul  22131  ressply1vsca  22132  subrgply1  22133  ply1plusgfvi  22142  psr1ring  22147  psr1lmod  22149  psr1sca  22150  ply1ascl  22160  subrg1ascl  22161  subrg1asclcl  22162  subrgvr1  22163  subrgvr1cl  22164  coe1z  22165  coe1mul2lem1  22169  coe1mul2  22171  coe1tm  22175  evls1val  22223  evls1rhm  22225  evls1sca  22226  evl1val  22232  evl1rhm  22235  evl1sca  22237  evl1var  22239  evls1var  22241  mpfpf1  22254  pf1mpf  22255  pf1ind  22258  xkofvcn  23587  xpstopnlem1  23712  ufildom1  23829  deg1z  26008  deg1addle  26022  deg1vscale  26025  deg1vsca  26026  deg1mulle2  26030  deg1le0  26032  ply1nzb  26044  sltval2  27584  noextendlt  27597  sltsolem1  27603  nosepnelem  27607  nolt02o  27623  old1  27807  rankeq1o  36147  ssoninhaus  36424  onint1  36425  1oequni2o  37344  finxp1o  37368  finxpreclem3  37369  finxpreclem4  37370  finxpreclem5  37371  finxpsuclem  37373  pw2f1ocnv  43013  wepwsolem  43018  pwfi2f1o  43072  oaabsb  43270  oaordnr  43272  omnord1  43281  oege1  43282  oaomoencom  43293  omabs2  43308  omcl3g  43310  nadd1suc  43368  om2  43380  oe2  43382  safesnsupfiss  43391  safesnsupfidom1o  43393  safesnsupfilb  43394  1no  43412  nlim2NEW  43419  oa1cl  43423  sn1dom  43502  pr2dom  43503  tr3dom  43504  clsk1indlem4  44020