Theorem 1on 8516

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8504	. 2 ⊢ 1o = suc ∅
2		0elon 6439	. . 3 ⊢ ∅ ∈ On
3		1oex 8514	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2835	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7828	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2834	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2105  Vcvv 3477  ∅c0 4338  Oncon0 6385  suc csuc 6387  1_oc1o 8497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-on 6389  df-suc 6391  df-1o 8504

This theorem is referenced by:  2on  8518  2onOLD  8519  nlim2  8526  ord1eln01  8532  ondif2  8538  2oconcl  8539  fnoe  8546  oesuclem  8561  oecl  8573  o1p1e2  8576  om1r  8579  oe1m  8581  omword1  8609  omword2  8610  omlimcl  8614  oneo  8617  oewordi  8627  oelim2  8631  oeoa  8633  oeoe  8635  oeeui  8638  1onn  8676  oaabs2  8685  enpr2dOLD  9088  sucxpdom  9288  en2  9312  oancom  9688  cnfcom3lem  9740  ssttrcl  9752  ttrcltr  9753  dmttrcl  9758  ttrclselem2  9763  pm54.43lem  10037  pm54.43  10038  infxpenc  10055  infxpenc2  10059  undjudom  10205  endjudisj  10206  djuen  10207  dju1p1e2  10211  dju1p1e2ALT  10212  xpdjuen  10217  mapdjuen  10218  djuxpdom  10223  djufi  10224  djuinf  10226  infdju1  10227  pwdju1  10228  pwdjudom  10252  isfin4p1  10352  pwxpndom2  10702  wunex2  10775  wuncval2  10784  tsk2  10802  efgmnvl  19746  frgpnabllem1  19905  dmdprdpr  20083  dprdpr  20084  psr1crng  22203  psr1assa  22204  psr1tos  22205  psr1bas  22207  vr1cl2  22209  ply1lss  22213  ply1subrg  22214  ply1ass23l  22243  ressply1bas2  22244  ressply1add  22246  ressply1mul  22247  ressply1vsca  22248  subrgply1  22249  ply1plusgfvi  22258  psr1ring  22263  psr1lmod  22265  psr1sca  22266  ply1ascl  22276  subrg1ascl  22277  subrg1asclcl  22278  subrgvr1  22279  subrgvr1cl  22280  coe1z  22281  coe1mul2lem1  22285  coe1mul2  22287  coe1tm  22291  evls1val  22339  evls1rhm  22341  evls1sca  22342  evl1val  22348  evl1rhm  22351  evl1sca  22353  evl1var  22355  evls1var  22357  mpfpf1  22370  pf1mpf  22371  pf1ind  22374  xkofvcn  23707  xpstopnlem1  23832  ufildom1  23949  deg1z  26140  deg1addle  26154  deg1vscale  26157  deg1vsca  26158  deg1mulle2  26162  deg1le0  26164  ply1nzb  26176  sltval2  27715  noextendlt  27728  sltsolem1  27734  nosepnelem  27738  nolt02o  27754  old1  27928  rankeq1o  36152  ssoninhaus  36430  onint1  36431  1oequni2o  37350  finxp1o  37374  finxpreclem3  37375  finxpreclem4  37376  finxpreclem5  37377  finxpsuclem  37379  pw2f1ocnv  43025  wepwsolem  43030  pwfi2f1o  43084  oaabsb  43283  oaordnr  43285  omnord1  43294  oege1  43295  oaomoencom  43306  omabs2  43321  omcl3g  43323  nadd1suc  43381  om2  43393  oe2  43395  safesnsupfiss  43404  safesnsupfidom1o  43406  safesnsupfilb  43407  1no  43425  nlim2NEW  43432  oa1cl  43436  sn1dom  43515  pr2dom  43516  tr3dom  43517  clsk1indlem4  44033