Theorem 1on 8408

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 8396	. 2 ⊢ 1o = suc ∅
2		0elon 6370	. . 3 ⊢ ∅ ∈ On
3		1oex 8406	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2834	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7754	. . 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 6315  suc csuc 6317  1_oc1o 8389

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 5368

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 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319  df-suc 6321  df-1o 8396

This theorem is referenced by:  2on  8409  nlim2  8416  ord1eln01  8422  ondif2  8428  2oconcl  8429  fnoe  8436  oesuclem  8451  oecl  8463  o1p1e2  8466  om1r  8469  oe1m  8471  omword1  8499  omword2  8500  omlimcl  8504  oneo  8507  om2  8512  oewordi  8518  oelim2  8522  oeoa  8524  oeoe  8526  oeeui  8529  1onn  8567  oaabs2  8576  sucxpdom  9162  en2  9181  oancom  9561  cnfcom3lem  9613  ssttrcl  9625  ttrcltr  9626  dmttrcl  9631  ttrclselem2  9636  pm54.43lem  9913  pm54.43  9914  infxpenc  9929  infxpenc2  9933  undjudom  10079  endjudisj  10080  djuen  10081  dju1p1e2  10085  dju1p1e2ALT  10086  xpdjuen  10091  mapdjuen  10092  djuxpdom  10097  djufi  10098  djuinf  10100  infdju1  10101  pwdju1  10102  pwdjudom  10126  isfin4p1  10226  pwxpndom2  10577  wunex2  10650  wuncval2  10659  tsk2  10677  efgmnvl  19678  frgpnabllem1  19837  dmdprdpr  20015  dprdpr  20016  psr1crng  22158  psr1assa  22159  psr1tos  22160  psr1bas  22162  vr1cl2  22164  ply1lss  22168  ply1subrg  22169  ply1ass23l  22198  ressply1bas2  22199  ressply1add  22201  ressply1mul  22202  ressply1vsca  22203  subrgply1  22204  ply1plusgfvi  22213  psr1ring  22218  psr1lmod  22220  psr1sca  22221  ply1ascl  22231  subrg1ascl  22232  subrg1asclcl  22233  subrgvr1  22234  subrgvr1cl  22235  coe1z  22236  coe1mul2lem1  22240  coe1mul2  22242  coe1tm  22246  evls1val  22293  evls1rhm  22295  evls1sca  22296  evl1val  22302  evl1rhm  22305  evl1sca  22307  evl1var  22309  evls1var  22311  mpfpf1  22324  pf1mpf  22325  pf1ind  22328  xkofvcn  23657  xpstopnlem1  23782  ufildom1  23899  deg1z  26060  deg1addle  26074  deg1vscale  26077  deg1vsca  26078  deg1mulle2  26082  deg1le0  26084  ply1nzb  26096  ltsval2  27632  noextendlt  27645  ltssolem1  27651  nosepnelem  27655  nolt02o  27671  old1  27869  rankeq1o  36367  ssoninhaus  36644  onint1  36645  1oequni2o  37688  finxp1o  37712  finxpreclem3  37713  finxpreclem4  37714  finxpreclem5  37715  finxpsuclem  37717  pw2f1ocnv  43473  wepwsolem  43478  pwfi2f1o  43532  oaabsb  43730  oaordnr  43732  omnord1  43741  oege1  43742  oaomoencom  43753  omabs2  43768  omcl3g  43770  nadd1suc  43828  oe2  43841  safesnsupfiss  43850  safesnsupfidom1o  43852  safesnsupfilb  43853  1fno  43871  nlim2NEW  43878  oa1cl  43882  sn1dom  43961  pr2dom  43962  tr3dom  43963  clsk1indlem4  44479