Theorem 1on 8478

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8466	. 2 ⊢ 1o = suc ∅
2		0elon 6419	. . 3 ⊢ ∅ ∈ On
3		1oex 8476	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2831	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7797	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 691	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2830	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2107  Vcvv 3475  ∅c0 4323  Oncon0 6365  suc csuc 6367  1_oc1o 8459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-on 6369  df-suc 6371  df-1o 8466

This theorem is referenced by:  2on  8480  2onOLD  8481  1oexOLD  8486  nlim2  8490  ord1eln01  8496  ondif2  8502  2oconcl  8503  fnoe  8510  oesuclem  8525  oecl  8537  o1p1e2  8540  om1r  8543  oe1m  8545  omword1  8573  omword2  8574  omlimcl  8578  oneo  8581  oewordi  8591  oelim2  8595  oeoa  8597  oeoe  8599  oeeui  8602  1onn  8639  oaabs2  8648  enpr2dOLD  9050  sucxpdom  9255  en2  9281  oancom  9646  cnfcom3lem  9698  ssttrcl  9710  ttrcltr  9711  dmttrcl  9716  ttrclselem2  9721  pm54.43lem  9995  pm54.43  9996  infxpenc  10013  infxpenc2  10017  undjudom  10162  endjudisj  10163  djuen  10164  dju1p1e2  10168  dju1p1e2ALT  10169  xpdjuen  10174  mapdjuen  10175  djuxpdom  10180  djufi  10181  djuinf  10183  infdju1  10184  pwdju1  10185  pwdjudom  10211  isfin4p1  10310  pwxpndom2  10660  wunex2  10733  wuncval2  10742  tsk2  10760  efgmnvl  19582  frgpnabllem1  19741  dmdprdpr  19919  dprdpr  19920  psr1crng  21711  psr1assa  21712  psr1tos  21713  psr1bas  21715  vr1cl2  21717  ply1lss  21720  ply1subrg  21721  ressply1bas2  21750  ressply1add  21752  ressply1mul  21753  ressply1vsca  21754  subrgply1  21755  ply1plusgfvi  21764  psr1ring  21769  psr1lmod  21771  psr1sca  21772  ply1ascl  21780  subrg1ascl  21781  subrg1asclcl  21782  subrgvr1  21783  subrgvr1cl  21784  coe1z  21785  coe1mul2lem1  21789  coe1mul2  21791  coe1tm  21795  evls1val  21839  evls1rhm  21841  evls1sca  21842  evl1val  21848  evl1rhm  21851  evl1sca  21853  evl1var  21855  evls1var  21857  mpfpf1  21870  pf1mpf  21871  pf1ind  21874  xkofvcn  23188  xpstopnlem1  23313  ufildom1  23430  deg1z  25605  deg1addle  25619  deg1vscale  25622  deg1vsca  25623  deg1mulle2  25627  deg1le0  25629  ply1nzb  25640  sltval2  27159  noextendlt  27172  sltsolem1  27178  nosepnelem  27182  nolt02o  27198  old1  27370  rankeq1o  35143  ssoninhaus  35333  onint1  35334  1oequni2o  36249  finxp1o  36273  finxpreclem3  36274  finxpreclem4  36275  finxpreclem5  36276  finxpsuclem  36278  pw2f1ocnv  41776  wepwsolem  41784  pwfi2f1o  41838  oaabsb  42044  oaordnr  42046  omnord1  42055  oege1  42056  oaomoencom  42067  omabs2  42082  omcl3g  42084  nadd1suc  42142  om2  42155  oe2  42157  safesnsupfiss  42166  safesnsupfidom1o  42168  safesnsupfilb  42169  1no  42187  nlim2NEW  42194  oa1cl  42198  sn1dom  42277  pr2dom  42278  tr3dom  42279  clsk1indlem4  42795  ply1ass23l  47063