Theorem 1on 8518

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8506	. 2 ⊢ 1o = suc ∅
2		0elon 6438	. . 3 ⊢ ∅ ∈ On
3		1oex 8516	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2838	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7829	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2837	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2108  Vcvv 3480  ∅c0 4333  Oncon0 6384  suc csuc 6386  1_oc1o 8499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-suc 6390  df-1o 8506

This theorem is referenced by:  2on  8520  2onOLD  8521  nlim2  8528  ord1eln01  8534  ondif2  8540  2oconcl  8541  fnoe  8548  oesuclem  8563  oecl  8575  o1p1e2  8578  om1r  8581  oe1m  8583  omword1  8611  omword2  8612  omlimcl  8616  oneo  8619  oewordi  8629  oelim2  8633  oeoa  8635  oeoe  8637  oeeui  8640  1onn  8678  oaabs2  8687  enpr2dOLD  9090  sucxpdom  9291  en2  9315  oancom  9691  cnfcom3lem  9743  ssttrcl  9755  ttrcltr  9756  dmttrcl  9761  ttrclselem2  9766  pm54.43lem  10040  pm54.43  10041  infxpenc  10058  infxpenc2  10062  undjudom  10208  endjudisj  10209  djuen  10210  dju1p1e2  10214  dju1p1e2ALT  10215  xpdjuen  10220  mapdjuen  10221  djuxpdom  10226  djufi  10227  djuinf  10229  infdju1  10230  pwdju1  10231  pwdjudom  10255  isfin4p1  10355  pwxpndom2  10705  wunex2  10778  wuncval2  10787  tsk2  10805  efgmnvl  19732  frgpnabllem1  19891  dmdprdpr  20069  dprdpr  20070  psr1crng  22188  psr1assa  22189  psr1tos  22190  psr1bas  22192  vr1cl2  22194  ply1lss  22198  ply1subrg  22199  ply1ass23l  22228  ressply1bas2  22229  ressply1add  22231  ressply1mul  22232  ressply1vsca  22233  subrgply1  22234  ply1plusgfvi  22243  psr1ring  22248  psr1lmod  22250  psr1sca  22251  ply1ascl  22261  subrg1ascl  22262  subrg1asclcl  22263  subrgvr1  22264  subrgvr1cl  22265  coe1z  22266  coe1mul2lem1  22270  coe1mul2  22272  coe1tm  22276  evls1val  22324  evls1rhm  22326  evls1sca  22327  evl1val  22333  evl1rhm  22336  evl1sca  22338  evl1var  22340  evls1var  22342  mpfpf1  22355  pf1mpf  22356  pf1ind  22359  xkofvcn  23692  xpstopnlem1  23817  ufildom1  23934  deg1z  26126  deg1addle  26140  deg1vscale  26143  deg1vsca  26144  deg1mulle2  26148  deg1le0  26150  ply1nzb  26162  sltval2  27701  noextendlt  27714  sltsolem1  27720  nosepnelem  27724  nolt02o  27740  old1  27914  rankeq1o  36172  ssoninhaus  36449  onint1  36450  1oequni2o  37369  finxp1o  37393  finxpreclem3  37394  finxpreclem4  37395  finxpreclem5  37396  finxpsuclem  37398  pw2f1ocnv  43049  wepwsolem  43054  pwfi2f1o  43108  oaabsb  43307  oaordnr  43309  omnord1  43318  oege1  43319  oaomoencom  43330  omabs2  43345  omcl3g  43347  nadd1suc  43405  om2  43417  oe2  43419  safesnsupfiss  43428  safesnsupfidom1o  43430  safesnsupfilb  43431  1no  43449  nlim2NEW  43456  oa1cl  43460  sn1dom  43539  pr2dom  43540  tr3dom  43541  clsk1indlem4  44057