Theorem 1on 8468

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8455	. 2 ⊢ 1o = suc ∅
2		0elon 6420	. . 3 ⊢ ∅ ∈ On
3		1oex 8465	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2862	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7810	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 705	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2861	1 ⊢ 1o ∈ On

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  ∅c0 4286  Oncon0 6364  suc csuc 6366  1_oc1o 8448

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368  df-suc 6370  df-1o 8455

This theorem is used by:  2on  8469  nlim2  8477  ord1eln01  8483  ondif2  8489  2oconcl  8490  fnoe  8497  oesuclem  8512  oecl  8524  o1p1e2  8527  om1r  8530  oe1m  8532  omword1  8560  omword2  8561  omlimcl  8565  oneo  8568  om2  8573  oewordi  8579  oelim2  8583  oeoa  8585  oeoe  8587  oeeui  8590  1onn  8628  oaabs2  8637  sucxpdom  9224  en2  9243  oancom  9623  cnfcom3lem  9675  ssttrcl  9687  ttrcltr  9688  dmttrcl  9693  ttrclselem2  9698  pm54.43lem  9998  pm54.43  9999  infxpenc  10014  infxpenc2  10018  undjudom  10163  endjudisj  10164  djuen  10165  dju1p1e2  10169  dju1p1e2ALT  10170  xpdjuen  10175  mapdjuen  10176  djuxpdom  10181  djufi  10182  djuinf  10184  infdju1  10185  pwdju1  10186  pwdjudom  10210  isfin4p1  10310  pwxpndom2  10661  wunex2  10734  wuncval2  10743  tsk2  10761  efgmnvl  19807  frgpnabllem1  19966  dmdprdpr  20144  dprdpr  20145  psr1crng  22376  psr1assa  22377  psr1tos  22378  psr1bas  22380  vr1cl2  22382  ply1lss  22385  ply1subrg  22386  ply1ass23l  22415  ressply1bas2  22416  ressply1add  22418  ressply1mul  22419  ressply1vsca  22420  subrgply1  22421  ply1plusgfvi  22430  psr1ring  22435  psr1lmod  22437  psr1sca  22438  ply1ascl  22448  subrg1ascl  22449  subrg1asclcl  22450  subrgvr1  22451  subrgvr1cl  22452  coe1z  22453  coe1mul2lem1  22457  coe1mul2  22459  coe1tm  22463  evls1val  22509  evls1rhm  22511  evls1sca  22512  evl1val  22518  evl1rhm  22521  evl1sca  22523  evl1var  22525  evls1var  22527  mpfpf1  22540  pf1mpf  22541  pf1ind  22544  xkofvcn  23870  xpstopnlem1  23995  ufildom1  24112  deg1z  26273  deg1addle  26287  deg1vscale  26290  deg1vsca  26291  deg1mulle2  26295  deg1le0  26297  ply1nzb  26309  ltsval2  27849  noextendlt  27862  ltssolem1  27868  nosepnelem  27872  nolt02o  27888  old1  28087  rankeq1o  36676  nmulrid  36702  nmullid  36703  ssoninhaus  36992  onint1  36993  1oequni2o  38047  finxp1o  38071  finxpreclem3  38072  finxpreclem4  38073  finxpreclem5  38074  finxpsuclem  38076  pw2f1ocnv  43797  wepwsolem  43802  pwfi2f1o  43856  oaabsb  44054  oaordnr  44056  omnord1  44065  oege1  44066  oaomoencom  44077  omabs2  44092  omcl3g  44094  nadd1suc  44152  oe2  44165  safesnsupfiss  44174  safesnsupfidom1o  44176  safesnsupfilb  44177  1fno  44195  nlim2NEW  44202  oa1cl  44206  sn1dom  44285  pr2dom  44286  tr3dom  44287  clsk1indlem4  44803  setc1onsubc  50413