Theorem 1on 8468

Description: Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) Avoid ax-un 7736. (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 6413	. . 3 ⊢ ∅ ∈ On
3		1oex 8465	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2857	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7808	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 705	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2856	1 ⊢ 1o ∈ On

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  ∅c0 4279  Oncon0 6357  suc csuc 6359  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 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6360  df-on 6361  df-suc 6363  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  9231  en2  9250  oancom  9630  cnfcom3lem  9682  ssttrcl  9694  ttrcltr  9695  dmttrcl  9700  ttrclselem2  9705  pm54.43lem  10005  pm54.43  10006  infxpenc  10021  infxpenc2  10025  undjudom  10170  endjudisj  10171  djuen  10172  dju1p1e2  10176  dju1p1e2ALT  10177  xpdjuen  10182  mapdjuen  10183  djuxpdom  10188  djufi  10189  djuinf  10191  infdju1  10192  pwdju1  10193  pwdjudom  10217  isfin4p1  10317  pwxpndom2  10674  wunex2  10747  wuncval2  10756  tsk2  10774  efgmnvl  19841  frgpnabllem1  20000  dmdprdpr  20178  dprdpr  20179  psr1crng  22412  psr1assa  22413  psr1tos  22414  psr1bas  22416  vr1cl2  22418  ply1lss  22421  ply1subrg  22422  ply1ass23l  22451  ressply1bas2  22452  ressply1add  22454  ressply1mul  22455  ressply1vsca  22456  subrgply1  22457  ply1plusgfvi  22466  psr1ring  22471  psr1lmod  22473  psr1sca  22474  ply1ascl  22484  subrg1ascl  22485  subrg1asclcl  22486  subrgvr1  22487  subrgvr1cl  22488  coe1z  22489  coe1mul2lem1  22493  coe1mul2  22495  coe1tm  22499  evls1val  22545  evls1rhm  22547  evls1sca  22548  evl1val  22554  evl1rhm  22557  evl1sca  22559  evl1var  22561  evls1var  22563  mpfpf1  22576  pf1mpf  22577  pf1ind  22580  xkofvcn  23910  xpstopnlem1  24035  ufildom1  24152  deg1z  26312  deg1addle  26326  deg1vscale  26329  deg1vsca  26330  deg1mulle2  26334  deg1le0  26336  ply1nzb  26348  ltsval2  27892  noextendlt  27905  ltssolem1  27911  nosepnelem  27915  nolt02o  27931  old1  28130  rankeq1o  36751  nmulrid  36777  nmullid  36778  ssoninhaus  37067  onint1  37068  1oequni2o  38122  finxp1o  38146  finxpreclem3  38147  finxpreclem4  38148  finxpreclem5  38149  finxpsuclem  38151  pw2f1ocnv  43878  wepwsolem  43883  pwfi2f1o  43937  oaabsb  44135  oaordnr  44137  omnord1  44146  oege1  44147  oaomoencom  44158  omabs2  44173  omcl3g  44175  nadd1suc  44233  oe2  44246  safesnsupfiss  44255  safesnsupfidom1o  44257  safesnsupfilb  44258  1fno  44276  nlim2NEW  44283  oa1cl  44287  sn1dom  44366  pr2dom  44367  tr3dom  44368  clsk1indlem4  44884  setc1onsubc  50528