Theorem 1on 8467

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8454	. 2 ⊢ 1o = suc ∅
2		0elon 6418	. . 3 ⊢ ∅ ∈ On
3		1oex 8464	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2860	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7809	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 704	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2859	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ∅c0 4287  Oncon0 6362  suc csuc 6364  1_oc1o 8447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-tr 5220  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6365  df-on 6366  df-suc 6368  df-1o 8454

This theorem is referenced by:  2on  8468  nlim2  8476  ord1eln01  8482  ondif2  8488  2oconcl  8489  fnoe  8496  oesuclem  8511  oecl  8523  o1p1e2  8526  om1r  8529  oe1m  8531  omword1  8559  omword2  8560  omlimcl  8564  oneo  8567  om2  8572  oewordi  8578  oelim2  8582  oeoa  8584  oeoe  8586  oeeui  8589  1onn  8627  oaabs2  8636  sucxpdom  9222  en2  9241  oancom  9621  cnfcom3lem  9673  ssttrcl  9685  ttrcltr  9686  dmttrcl  9691  ttrclselem2  9696  pm54.43lem  9987  pm54.43  9988  infxpenc  10003  infxpenc2  10007  undjudom  10152  endjudisj  10153  djuen  10154  dju1p1e2  10158  dju1p1e2ALT  10159  xpdjuen  10164  mapdjuen  10165  djuxpdom  10170  djufi  10171  djuinf  10173  infdju1  10174  pwdju1  10175  pwdjudom  10199  isfin4p1  10300  pwxpndom2  10651  wunex2  10724  wuncval2  10733  tsk2  10751  efgmnvl  19785  frgpnabllem1  19944  dmdprdpr  20122  dprdpr  20123  psr1crng  22328  psr1assa  22329  psr1tos  22330  psr1bas  22332  vr1cl2  22334  ply1lss  22337  ply1subrg  22338  ply1ass23l  22367  ressply1bas2  22368  ressply1add  22370  ressply1mul  22371  ressply1vsca  22372  subrgply1  22373  ply1plusgfvi  22382  psr1ring  22387  psr1lmod  22389  psr1sca  22390  ply1ascl  22400  subrg1ascl  22401  subrg1asclcl  22402  subrgvr1  22403  subrgvr1cl  22404  coe1z  22405  coe1mul2lem1  22409  coe1mul2  22411  coe1tm  22415  evls1val  22461  evls1rhm  22463  evls1sca  22464  evl1val  22470  evl1rhm  22473  evl1sca  22475  evl1var  22477  evls1var  22479  mpfpf1  22492  pf1mpf  22493  pf1ind  22496  xkofvcn  23822  xpstopnlem1  23947  ufildom1  24064  deg1z  26225  deg1addle  26239  deg1vscale  26242  deg1vsca  26243  deg1mulle2  26247  deg1le0  26249  ply1nzb  26261  ltsval2  27801  noextendlt  27814  ltssolem1  27820  nosepnelem  27824  nolt02o  27840  old1  28039  rankeq1o  36644  nmulrid  36678  nmullid  36679  ssoninhaus  36940  onint1  36941  1oequni2o  37995  finxp1o  38019  finxpreclem3  38020  finxpreclem4  38021  finxpreclem5  38022  finxpsuclem  38024  pw2f1ocnv  43747  wepwsolem  43752  pwfi2f1o  43806  oaabsb  44004  oaordnr  44006  omnord1  44015  oege1  44016  oaomoencom  44027  omabs2  44042  omcl3g  44044  nadd1suc  44102  oe2  44115  safesnsupfiss  44124  safesnsupfidom1o  44126  safesnsupfilb  44127  1fno  44145  nlim2NEW  44152  oa1cl  44156  sn1dom  44235  pr2dom  44236  tr3dom  44237  clsk1indlem4  44753  setc1onsubc  50363