Theorem 1on 8475

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8463	. 2 ⊢ 1o = suc ∅
2		0elon 6416	. . 3 ⊢ ∅ ∈ On
3		1oex 8473	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2831	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7794	. . 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 4322  Oncon0 6362  suc csuc 6364  1_oc1o 8456

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 5299  ax-nul 5306  ax-pr 5427

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-ord 6365  df-on 6366  df-suc 6368  df-1o 8463

This theorem is referenced by:  2on  8477  2onOLD  8478  1oexOLD  8483  nlim2  8487  ord1eln01  8493  ondif2  8499  2oconcl  8500  fnoe  8507  oesuclem  8522  oecl  8534  o1p1e2  8537  om1r  8540  oe1m  8542  omword1  8570  omword2  8571  omlimcl  8575  oneo  8578  oewordi  8588  oelim2  8592  oeoa  8594  oeoe  8596  oeeui  8599  1onn  8636  oaabs2  8645  enpr2dOLD  9047  sucxpdom  9252  en2  9278  oancom  9643  cnfcom3lem  9695  ssttrcl  9707  ttrcltr  9708  dmttrcl  9713  ttrclselem2  9718  pm54.43lem  9992  pm54.43  9993  infxpenc  10010  infxpenc2  10014  undjudom  10159  endjudisj  10160  djuen  10161  dju1p1e2  10165  dju1p1e2ALT  10166  xpdjuen  10171  mapdjuen  10172  djuxpdom  10177  djufi  10178  djuinf  10180  infdju1  10181  pwdju1  10182  pwdjudom  10208  isfin4p1  10307  pwxpndom2  10657  wunex2  10730  wuncval2  10739  tsk2  10757  efgmnvl  19577  frgpnabllem1  19736  dmdprdpr  19914  dprdpr  19915  psr1crng  21703  psr1assa  21704  psr1tos  21705  psr1bas  21707  vr1cl2  21709  ply1lss  21712  ply1subrg  21713  ressply1bas2  21742  ressply1add  21744  ressply1mul  21745  ressply1vsca  21746  subrgply1  21747  ply1plusgfvi  21756  psr1ring  21761  psr1lmod  21763  psr1sca  21764  ply1ascl  21772  subrg1ascl  21773  subrg1asclcl  21774  subrgvr1  21775  subrgvr1cl  21776  coe1z  21777  coe1mul2lem1  21781  coe1mul2  21783  coe1tm  21787  evls1val  21831  evls1rhm  21833  evls1sca  21834  evl1val  21840  evl1rhm  21843  evl1sca  21845  evl1var  21847  evls1var  21849  mpfpf1  21862  pf1mpf  21863  pf1ind  21866  xkofvcn  23180  xpstopnlem1  23305  ufildom1  23422  deg1z  25597  deg1addle  25611  deg1vscale  25614  deg1vsca  25615  deg1mulle2  25619  deg1le0  25621  ply1nzb  25632  sltval2  27149  noextendlt  27162  sltsolem1  27168  nosepnelem  27172  nolt02o  27188  old1  27360  rankeq1o  35132  ssoninhaus  35322  onint1  35323  1oequni2o  36238  finxp1o  36262  finxpreclem3  36263  finxpreclem4  36264  finxpreclem5  36265  finxpsuclem  36267  pw2f1ocnv  41762  wepwsolem  41770  pwfi2f1o  41824  oaabsb  42030  oaordnr  42032  omnord1  42041  oege1  42042  oaomoencom  42053  omabs2  42068  omcl3g  42070  nadd1suc  42128  om2  42141  oe2  42143  safesnsupfiss  42152  safesnsupfidom1o  42154  safesnsupfilb  42155  1no  42173  nlim2NEW  42180  oa1cl  42184  sn1dom  42263  pr2dom  42264  tr3dom  42265  clsk1indlem4  42781  ply1ass23l  47017