Theorem 1on 8489

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8476	. 2 ⊢ 1o = suc ∅
2		0elon 6418	. . 3 ⊢ ∅ ∈ On
3		1oex 8486	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2858	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7823	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 705	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2857	1 ⊢ 1o ∈ On

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ∅c0 4279  Oncon0 6362  suc csuc 6364  1_oc1o 8469

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6365  df-on 6366  df-suc 6368  df-1o 8476

This theorem is used by:  2on  8490  nlim2  8498  ord1eln01  8504  ondif2  8510  2oconcl  8511  fnoe  8518  oesuclem  8533  oecl  8545  o1p1e2  8548  om1r  8551  oe1m  8553  omword1  8581  omword2  8582  omlimcl  8586  oneo  8589  om2  8594  oewordi  8600  oelim2  8604  oeoa  8606  oeoe  8608  oeeui  8611  1onn  8649  oaabs2  8658  sucxpdom  9252  en2  9271  oancom  9652  cnfcom3lem  9704  ssttrcl  9716  ttrcltr  9717  dmttrcl  9722  ttrclselem2  9727  pm54.43lem  10081  pm54.43  10082  infxpenc  10097  infxpenc2  10101  undjudom  10246  endjudisj  10247  djuen  10248  dju1p1e2  10252  dju1p1e2ALT  10253  xpdjuen  10258  mapdjuen  10259  djuxpdom  10264  djufi  10265  djuinf  10267  infdju1  10268  pwdju1  10269  pwdjudom  10293  isfin4p1  10393  pwxpndom2  10750  wunex2  10823  wuncval2  10832  tsk2  10850  efgmnvl  19928  frgpnabllem1  20087  dmdprdpr  20265  dprdpr  20266  psr1crng  22505  psr1assa  22506  psr1tos  22507  psr1bas  22509  vr1cl2  22511  ply1lss  22514  ply1subrg  22515  ply1ass23l  22544  ressply1bas2  22545  ressply1add  22547  ressply1mul  22548  ressply1vsca  22549  subrgply1  22550  ply1plusgfvi  22559  psr1ring  22564  psr1lmod  22566  psr1sca  22567  ply1ascl  22577  subrg1ascl  22578  subrg1asclcl  22579  subrgvr1  22580  subrgvr1cl  22581  coe1z  22582  coe1mul2lem1  22586  coe1mul2  22588  coe1tm  22592  evls1val  22638  evls1rhm  22640  evls1sca  22641  evl1val  22647  evl1rhm  22650  evl1sca  22652  evl1var  22654  evls1var  22656  mpfpf1  22669  pf1mpf  22670  pf1ind  22673  xkofvcn  24003  xpstopnlem1  24128  ufildom1  24245  deg1z  26405  deg1addle  26419  deg1vscale  26422  deg1vsca  26423  deg1mulle2  26427  deg1le0  26429  ply1nzb  26441  ltsval2  28013  noextendlt  28026  ltssolem1  28032  nosepnelem  28036  nolt02o  28052  old1  28251  rankeq1o  36932  nmulrid  36946  nmullid  36947  ssoninhaus  37236  onint1  37237  1oequni2o  38291  finxp1o  38315  finxpreclem3  38316  finxpreclem4  38317  finxpreclem5  38318  finxpsuclem  38320  pw2f1ocnv  44043  wepwsolem  44048  pwfi2f1o  44097  oaabsb  44295  oaordnr  44297  omnord1  44306  oege1  44307  oaomoencom  44318  omabs2  44333  omcl3g  44335  nadd1suc  44393  oe2  44406  safesnsupfiss  44415  safesnsupfidom1o  44417  safesnsupfilb  44418  1fno  44436  nlim2NEW  44443  oa1cl  44447  sn1dom  44526  pr2dom  44527  tr3dom  44528  clsk1indlem4  45043  setc1onsubc  50709