Theorem 1on 8318

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8306	. 2 ⊢ 1o = suc ∅
2		0elon 6323	. . 3 ⊢ ∅ ∈ On
3		1oex 8316	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2837	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7667	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 689	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2836	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2107  Vcvv 3433  ∅c0 4257  Oncon0 6270  suc csuc 6272  1_oc1o 8299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-11 2155  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-tr 5193  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-ord 6273  df-on 6274  df-suc 6276  df-1o 8306

This theorem is referenced by:  2on  8320  2onOLD  8321  1oexOLD  8325  nlim2  8329  ord1eln01  8335  ondif2  8341  2oconcl  8342  fnoe  8349  oesuclem  8364  oecl  8376  o1p1e2  8379  o2p2e4OLD  8381  om1r  8383  oe1m  8385  omword1  8413  omword2  8414  omlimcl  8418  oneo  8421  oewordi  8431  oelim2  8435  oeoa  8437  oeoe  8439  oeeui  8442  1onn  8479  oaabs2  8488  enpr2d  8847  sucxpdom  9041  oancom  9418  cnfcom3lem  9470  ssttrcl  9482  ttrcltr  9483  dmttrcl  9488  ttrclselem2  9493  pm54.43lem  9767  pm54.43  9768  infxpenc  9783  infxpenc2  9787  undjudom  9932  endjudisj  9933  djuen  9934  dju1p1e2  9938  dju1p1e2ALT  9939  xpdjuen  9944  mapdjuen  9945  djuxpdom  9950  djufi  9951  djuinf  9953  infdju1  9954  pwdju1  9955  pwdjudom  9981  isfin4p1  10080  pwxpndom2  10430  wunex2  10503  wuncval2  10512  tsk2  10530  efgmnvl  19329  frgpnabllem1  19483  dmdprdpr  19661  dprdpr  19662  psr1crng  21367  psr1assa  21368  psr1tos  21369  psr1bas  21371  vr1cl2  21373  ply1lss  21376  ply1subrg  21377  ressply1bas2  21408  ressply1add  21410  ressply1mul  21411  ressply1vsca  21412  subrgply1  21413  ply1plusgfvi  21422  psr1ring  21427  psr1lmod  21429  psr1sca  21430  ply1ascl  21438  subrg1ascl  21439  subrg1asclcl  21440  subrgvr1  21441  subrgvr1cl  21442  coe1z  21443  coe1mul2lem1  21447  coe1mul2  21449  coe1tm  21453  evls1val  21495  evls1rhm  21497  evls1sca  21498  evl1val  21504  evl1rhm  21507  evl1sca  21509  evl1var  21511  evls1var  21513  mpfpf1  21526  pf1mpf  21527  pf1ind  21530  xkofvcn  22844  xpstopnlem1  22969  ufildom1  23086  deg1z  25261  deg1addle  25275  deg1vscale  25278  deg1vsca  25279  deg1mulle2  25283  deg1le0  25285  ply1nzb  25296  sltval2  33868  noextendlt  33881  sltsolem1  33887  nosepnelem  33891  nolt02o  33907  rankeq1o  34482  ssoninhaus  34646  onint1  34647  1oequni2o  35548  finxp1o  35572  finxpreclem3  35573  finxpreclem4  35574  finxpreclem5  35575  finxpsuclem  35577  pw2f1ocnv  40866  wepwsolem  40874  pwfi2f1o  40928  nlim2NEW  41057  oa1cl  41061  sn1dom  41140  pr2dom  41141  tr3dom  41142  clsk1indlem4  41661  ply1ass23l  45734