Theorem 1on 8371

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8359	. 2 ⊢ 1o = suc ∅
2		0elon 6349	. . 3 ⊢ ∅ ∈ On
3		1oex 8369	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2834	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7714	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 689	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2833	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2105  Vcvv 3441  ∅c0 4268  Oncon0 6296  suc csuc 6298  1_oc1o 8352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pr 5369

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-opab 5152  df-tr 5207  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-we 5571  df-ord 6299  df-on 6300  df-suc 6302  df-1o 8359

This theorem is referenced by:  2on  8373  2onOLD  8374  1oexOLD  8379  nlim2  8383  ord1eln01  8389  ondif2  8395  2oconcl  8396  fnoe  8403  oesuclem  8418  oecl  8430  o1p1e2  8433  o2p2e4OLD  8435  om1r  8437  oe1m  8439  omword1  8467  omword2  8468  omlimcl  8472  oneo  8475  oewordi  8485  oelim2  8489  oeoa  8491  oeoe  8493  oeeui  8496  1onn  8533  oaabs2  8542  enpr2dOLD  8907  sucxpdom  9112  en2  9138  oancom  9500  cnfcom3lem  9552  ssttrcl  9564  ttrcltr  9565  dmttrcl  9570  ttrclselem2  9575  pm54.43lem  9849  pm54.43  9850  infxpenc  9867  infxpenc2  9871  undjudom  10016  endjudisj  10017  djuen  10018  dju1p1e2  10022  dju1p1e2ALT  10023  xpdjuen  10028  mapdjuen  10029  djuxpdom  10034  djufi  10035  djuinf  10037  infdju1  10038  pwdju1  10039  pwdjudom  10065  isfin4p1  10164  pwxpndom2  10514  wunex2  10587  wuncval2  10596  tsk2  10614  efgmnvl  19407  frgpnabllem1  19561  dmdprdpr  19739  dprdpr  19740  psr1crng  21456  psr1assa  21457  psr1tos  21458  psr1bas  21460  vr1cl2  21462  ply1lss  21465  ply1subrg  21466  ressply1bas2  21497  ressply1add  21499  ressply1mul  21500  ressply1vsca  21501  subrgply1  21502  ply1plusgfvi  21511  psr1ring  21516  psr1lmod  21518  psr1sca  21519  ply1ascl  21527  subrg1ascl  21528  subrg1asclcl  21529  subrgvr1  21530  subrgvr1cl  21531  coe1z  21532  coe1mul2lem1  21536  coe1mul2  21538  coe1tm  21542  evls1val  21584  evls1rhm  21586  evls1sca  21587  evl1val  21593  evl1rhm  21596  evl1sca  21598  evl1var  21600  evls1var  21602  mpfpf1  21615  pf1mpf  21616  pf1ind  21619  xkofvcn  22933  xpstopnlem1  23058  ufildom1  23175  deg1z  25350  deg1addle  25364  deg1vscale  25367  deg1vsca  25368  deg1mulle2  25372  deg1le0  25374  ply1nzb  25385  sltval2  26902  noextendlt  26915  sltsolem1  26921  nosepnelem  26925  nolt02o  26941  rankeq1o  34564  ssoninhaus  34728  onint1  34729  1oequni2o  35637  finxp1o  35661  finxpreclem3  35662  finxpreclem4  35663  finxpreclem5  35664  finxpsuclem  35666  pw2f1ocnv  41110  wepwsolem  41118  pwfi2f1o  41172  omabs2  41305  omcl3g  41307  safesnsupfiss  41332  safesnsupfidom1o  41334  safesnsupfilb  41335  1no  41353  nlim2NEW  41360  oa1cl  41364  sn1dom  41443  pr2dom  41444  tr3dom  41445  clsk1indlem4  41964  ply1ass23l  46063