Theorem 1on 8392

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8380	. 2 ⊢ 1o = suc ∅
2		0elon 6356	. . 3 ⊢ ∅ ∈ On
3		1oex 8390	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2828	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7737	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2827	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ∅c0 4278  Oncon0 6301  suc csuc 6303  1_oc1o 8373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-ord 6304  df-on 6305  df-suc 6307  df-1o 8380

This theorem is referenced by:  2on  8393  nlim2  8400  ord1eln01  8406  ondif2  8412  2oconcl  8413  fnoe  8420  oesuclem  8435  oecl  8447  o1p1e2  8450  om1r  8453  oe1m  8455  omword1  8483  omword2  8484  omlimcl  8488  oneo  8491  oewordi  8501  oelim2  8505  oeoa  8507  oeoe  8509  oeeui  8512  1onn  8550  oaabs2  8559  sucxpdom  9140  en2  9159  oancom  9536  cnfcom3lem  9588  ssttrcl  9600  ttrcltr  9601  dmttrcl  9606  ttrclselem2  9611  pm54.43lem  9888  pm54.43  9889  infxpenc  9904  infxpenc2  9908  undjudom  10054  endjudisj  10055  djuen  10056  dju1p1e2  10060  dju1p1e2ALT  10061  xpdjuen  10066  mapdjuen  10067  djuxpdom  10072  djufi  10073  djuinf  10075  infdju1  10076  pwdju1  10077  pwdjudom  10101  isfin4p1  10201  pwxpndom2  10551  wunex2  10624  wuncval2  10633  tsk2  10651  efgmnvl  19621  frgpnabllem1  19780  dmdprdpr  19958  dprdpr  19959  psr1crng  22094  psr1assa  22095  psr1tos  22096  psr1bas  22098  vr1cl2  22100  ply1lss  22104  ply1subrg  22105  ply1ass23l  22134  ressply1bas2  22135  ressply1add  22137  ressply1mul  22138  ressply1vsca  22139  subrgply1  22140  ply1plusgfvi  22149  psr1ring  22154  psr1lmod  22156  psr1sca  22157  ply1ascl  22167  subrg1ascl  22168  subrg1asclcl  22169  subrgvr1  22170  subrgvr1cl  22171  coe1z  22172  coe1mul2lem1  22176  coe1mul2  22178  coe1tm  22182  evls1val  22230  evls1rhm  22232  evls1sca  22233  evl1val  22239  evl1rhm  22242  evl1sca  22244  evl1var  22246  evls1var  22248  mpfpf1  22261  pf1mpf  22262  pf1ind  22265  xkofvcn  23594  xpstopnlem1  23719  ufildom1  23836  deg1z  26014  deg1addle  26028  deg1vscale  26031  deg1vsca  26032  deg1mulle2  26036  deg1le0  26038  ply1nzb  26050  sltval2  27590  noextendlt  27603  sltsolem1  27609  nosepnelem  27613  nolt02o  27629  old1  27815  rankeq1o  36205  ssoninhaus  36482  onint1  36483  1oequni2o  37402  finxp1o  37426  finxpreclem3  37427  finxpreclem4  37428  finxpreclem5  37429  finxpsuclem  37431  pw2f1ocnv  43070  wepwsolem  43075  pwfi2f1o  43129  oaabsb  43327  oaordnr  43329  omnord1  43338  oege1  43339  oaomoencom  43350  omabs2  43365  omcl3g  43367  nadd1suc  43425  om2  43437  oe2  43439  safesnsupfiss  43448  safesnsupfidom1o  43450  safesnsupfilb  43451  1no  43469  nlim2NEW  43476  oa1cl  43480  sn1dom  43559  pr2dom  43560  tr3dom  43561  clsk1indlem4  44077