Theorem 1on 8417

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8405	. 2 ⊢ 1o = suc ∅
2		0elon 6378	. . 3 ⊢ ∅ ∈ On
3		1oex 8415	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2833	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7763	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 693	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2832	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ∅c0 4273  Oncon0 6323  suc csuc 6325  1_oc1o 8398

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-tr 5193  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6326  df-on 6327  df-suc 6329  df-1o 8405

This theorem is referenced by:  2on  8418  nlim2  8425  ord1eln01  8431  ondif2  8437  2oconcl  8438  fnoe  8445  oesuclem  8460  oecl  8472  o1p1e2  8475  om1r  8478  oe1m  8480  omword1  8508  omword2  8509  omlimcl  8513  oneo  8516  om2  8521  oewordi  8527  oelim2  8531  oeoa  8533  oeoe  8535  oeeui  8538  1onn  8576  oaabs2  8585  sucxpdom  9171  en2  9190  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  19689  frgpnabllem1  19848  dmdprdpr  20026  dprdpr  20027  psr1crng  22150  psr1assa  22151  psr1tos  22152  psr1bas  22154  vr1cl2  22156  ply1lss  22160  ply1subrg  22161  ply1ass23l  22190  ressply1bas2  22191  ressply1add  22193  ressply1mul  22194  ressply1vsca  22195  subrgply1  22196  ply1plusgfvi  22205  psr1ring  22210  psr1lmod  22212  psr1sca  22213  ply1ascl  22223  subrg1ascl  22224  subrg1asclcl  22225  subrgvr1  22226  subrgvr1cl  22227  coe1z  22228  coe1mul2lem1  22232  coe1mul2  22234  coe1tm  22238  evls1val  22285  evls1rhm  22287  evls1sca  22288  evl1val  22294  evl1rhm  22297  evl1sca  22299  evl1var  22301  evls1var  22303  mpfpf1  22316  pf1mpf  22317  pf1ind  22320  xkofvcn  23649  xpstopnlem1  23774  ufildom1  23891  deg1z  26052  deg1addle  26066  deg1vscale  26069  deg1vsca  26070  deg1mulle2  26074  deg1le0  26076  ply1nzb  26088  ltsval2  27620  noextendlt  27633  ltssolem1  27639  nosepnelem  27643  nolt02o  27659  old1  27857  rankeq1o  36353  ssoninhaus  36630  onint1  36631  1oequni2o  37684  finxp1o  37708  finxpreclem3  37709  finxpreclem4  37710  finxpreclem5  37711  finxpsuclem  37713  pw2f1ocnv  43465  wepwsolem  43470  pwfi2f1o  43524  oaabsb  43722  oaordnr  43724  omnord1  43733  oege1  43734  oaomoencom  43745  omabs2  43760  omcl3g  43762  nadd1suc  43820  oe2  43833  safesnsupfiss  43842  safesnsupfidom1o  43844  safesnsupfilb  43845  1fno  43863  nlim2NEW  43870  oa1cl  43874  sn1dom  43953  pr2dom  43954  tr3dom  43955  clsk1indlem4  44471  setc1onsubc  50077