Theorem 1on 8490

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8478	. 2 ⊢ 1o = suc ∅
2		0elon 6407	. . 3 ⊢ ∅ ∈ On
3		1oex 8488	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2831	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7801	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2830	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2108  Vcvv 3459  ∅c0 4308  Oncon0 6352  suc csuc 6354  1_oc1o 8471

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-tr 5230  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-ord 6355  df-on 6356  df-suc 6358  df-1o 8478

This theorem is referenced by:  2on  8492  2onOLD  8493  nlim2  8500  ord1eln01  8506  ondif2  8512  2oconcl  8513  fnoe  8520  oesuclem  8535  oecl  8547  o1p1e2  8550  om1r  8553  oe1m  8555  omword1  8583  omword2  8584  omlimcl  8588  oneo  8591  oewordi  8601  oelim2  8605  oeoa  8607  oeoe  8609  oeeui  8612  1onn  8650  oaabs2  8659  enpr2dOLD  9062  sucxpdom  9261  en2  9285  oancom  9663  cnfcom3lem  9715  ssttrcl  9727  ttrcltr  9728  dmttrcl  9733  ttrclselem2  9738  pm54.43lem  10012  pm54.43  10013  infxpenc  10030  infxpenc2  10034  undjudom  10180  endjudisj  10181  djuen  10182  dju1p1e2  10186  dju1p1e2ALT  10187  xpdjuen  10192  mapdjuen  10193  djuxpdom  10198  djufi  10199  djuinf  10201  infdju1  10202  pwdju1  10203  pwdjudom  10227  isfin4p1  10327  pwxpndom2  10677  wunex2  10750  wuncval2  10759  tsk2  10777  efgmnvl  19693  frgpnabllem1  19852  dmdprdpr  20030  dprdpr  20031  psr1crng  22120  psr1assa  22121  psr1tos  22122  psr1bas  22124  vr1cl2  22126  ply1lss  22130  ply1subrg  22131  ply1ass23l  22160  ressply1bas2  22161  ressply1add  22163  ressply1mul  22164  ressply1vsca  22165  subrgply1  22166  ply1plusgfvi  22175  psr1ring  22180  psr1lmod  22182  psr1sca  22183  ply1ascl  22193  subrg1ascl  22194  subrg1asclcl  22195  subrgvr1  22196  subrgvr1cl  22197  coe1z  22198  coe1mul2lem1  22202  coe1mul2  22204  coe1tm  22208  evls1val  22256  evls1rhm  22258  evls1sca  22259  evl1val  22265  evl1rhm  22268  evl1sca  22270  evl1var  22272  evls1var  22274  mpfpf1  22287  pf1mpf  22288  pf1ind  22291  xkofvcn  23620  xpstopnlem1  23745  ufildom1  23862  deg1z  26042  deg1addle  26056  deg1vscale  26059  deg1vsca  26060  deg1mulle2  26064  deg1le0  26066  ply1nzb  26078  sltval2  27618  noextendlt  27631  sltsolem1  27637  nosepnelem  27641  nolt02o  27657  old1  27831  rankeq1o  36135  ssoninhaus  36412  onint1  36413  1oequni2o  37332  finxp1o  37356  finxpreclem3  37357  finxpreclem4  37358  finxpreclem5  37359  finxpsuclem  37361  pw2f1ocnv  43008  wepwsolem  43013  pwfi2f1o  43067  oaabsb  43265  oaordnr  43267  omnord1  43276  oege1  43277  oaomoencom  43288  omabs2  43303  omcl3g  43305  nadd1suc  43363  om2  43375  oe2  43377  safesnsupfiss  43386  safesnsupfidom1o  43388  safesnsupfilb  43389  1no  43407  nlim2NEW  43414  oa1cl  43418  sn1dom  43497  pr2dom  43498  tr3dom  43499  clsk1indlem4  44015