Theorem 1on 8444

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8431	. 2 ⊢ 1o = suc ∅
2		0elon 6396	. . 3 ⊢ ∅ ∈ On
3		1oex 8441	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2858	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7787	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 702	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2857	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2141  Vcvv 3453  ∅c0 4283  Oncon0 6341  suc csuc 6343  1_oc1o 8424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-tr 5205  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-ord 6344  df-on 6345  df-suc 6347  df-1o 8431

This theorem is referenced by:  2on  8445  nlim2  8453  ord1eln01  8459  ondif2  8465  2oconcl  8466  fnoe  8473  oesuclem  8488  oecl  8500  o1p1e2  8503  om1r  8506  oe1m  8508  omword1  8536  omword2  8537  omlimcl  8541  oneo  8544  om2  8549  oewordi  8555  oelim2  8559  oeoa  8561  oeoe  8563  oeeui  8566  1onn  8604  oaabs2  8613  sucxpdom  9199  en2  9218  oancom  9600  cnfcom3lem  9652  ssttrcl  9664  ttrcltr  9665  dmttrcl  9670  ttrclselem2  9675  pm54.43lem  9952  pm54.43  9953  infxpenc  9968  infxpenc2  9972  undjudom  10118  endjudisj  10119  djuen  10120  dju1p1e2  10124  dju1p1e2ALT  10125  xpdjuen  10130  mapdjuen  10131  djuxpdom  10136  djufi  10137  djuinf  10139  infdju1  10140  pwdju1  10141  pwdjudom  10165  isfin4p1  10266  pwxpndom2  10617  wunex2  10690  wuncval2  10699  tsk2  10717  efgmnvl  19745  frgpnabllem1  19904  dmdprdpr  20082  dprdpr  20083  psr1crng  22237  psr1assa  22238  psr1tos  22239  psr1bas  22241  vr1cl2  22243  ply1lss  22246  ply1subrg  22247  ply1ass23l  22276  ressply1bas2  22277  ressply1add  22279  ressply1mul  22280  ressply1vsca  22281  subrgply1  22282  ply1plusgfvi  22291  psr1ring  22296  psr1lmod  22298  psr1sca  22299  ply1ascl  22309  subrg1ascl  22310  subrg1asclcl  22311  subrgvr1  22312  subrgvr1cl  22313  coe1z  22314  coe1mul2lem1  22318  coe1mul2  22320  coe1tm  22324  evls1val  22371  evls1rhm  22373  evls1sca  22374  evl1val  22380  evl1rhm  22383  evl1sca  22385  evl1var  22387  evls1var  22389  mpfpf1  22402  pf1mpf  22403  pf1ind  22406  xkofvcn  23732  xpstopnlem1  23857  ufildom1  23974  deg1z  26135  deg1addle  26149  deg1vscale  26152  deg1vsca  26153  deg1mulle2  26157  deg1le0  26159  ply1nzb  26171  ltsval2  27708  noextendlt  27721  ltssolem1  27727  nosepnelem  27731  nolt02o  27747  old1  27946  rankeq1o  36482  ssoninhaus  36769  onint1  36770  1oequni2o  37823  finxp1o  37847  finxpreclem3  37848  finxpreclem4  37849  finxpreclem5  37850  finxpsuclem  37852  pw2f1ocnv  43575  wepwsolem  43580  pwfi2f1o  43634  oaabsb  43832  oaordnr  43834  omnord1  43843  oege1  43844  oaomoencom  43855  omabs2  43870  omcl3g  43872  nadd1suc  43930  oe2  43943  safesnsupfiss  43952  safesnsupfidom1o  43954  safesnsupfilb  43955  1fno  43973  nlim2NEW  43980  oa1cl  43984  sn1dom  44063  pr2dom  44064  tr3dom  44065  clsk1indlem4  44581  setc1onsubc  50184