Theorem 1on 8406

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8394	. 2 ⊢ 1o = suc ∅
2		0elon 6369	. . 3 ⊢ ∅ ∈ On
3		1oex 8404	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2830	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7751	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2829	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2113  Vcvv 3437  ∅c0 4282  Oncon0 6314  suc csuc 6316  1_oc1o 8387

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 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317  df-on 6318  df-suc 6320  df-1o 8394

This theorem is referenced by:  2on  8407  nlim2  8414  ord1eln01  8420  ondif2  8426  2oconcl  8427  fnoe  8434  oesuclem  8449  oecl  8461  o1p1e2  8464  om1r  8467  oe1m  8469  omword1  8497  omword2  8498  omlimcl  8502  oneo  8505  oewordi  8515  oelim2  8519  oeoa  8521  oeoe  8523  oeeui  8526  1onn  8564  oaabs2  8573  sucxpdom  9156  en2  9175  oancom  9552  cnfcom3lem  9604  ssttrcl  9616  ttrcltr  9617  dmttrcl  9622  ttrclselem2  9627  pm54.43lem  9904  pm54.43  9905  infxpenc  9920  infxpenc2  9924  undjudom  10070  endjudisj  10071  djuen  10072  dju1p1e2  10076  dju1p1e2ALT  10077  xpdjuen  10082  mapdjuen  10083  djuxpdom  10088  djufi  10089  djuinf  10091  infdju1  10092  pwdju1  10093  pwdjudom  10117  isfin4p1  10217  pwxpndom2  10567  wunex2  10640  wuncval2  10649  tsk2  10667  efgmnvl  19634  frgpnabllem1  19793  dmdprdpr  19971  dprdpr  19972  psr1crng  22118  psr1assa  22119  psr1tos  22120  psr1bas  22122  vr1cl2  22124  ply1lss  22128  ply1subrg  22129  ply1ass23l  22158  ressply1bas2  22159  ressply1add  22161  ressply1mul  22162  ressply1vsca  22163  subrgply1  22164  ply1plusgfvi  22173  psr1ring  22178  psr1lmod  22180  psr1sca  22181  ply1ascl  22191  subrg1ascl  22192  subrg1asclcl  22193  subrgvr1  22194  subrgvr1cl  22195  coe1z  22196  coe1mul2lem1  22200  coe1mul2  22202  coe1tm  22206  evls1val  22255  evls1rhm  22257  evls1sca  22258  evl1val  22264  evl1rhm  22267  evl1sca  22269  evl1var  22271  evls1var  22273  mpfpf1  22286  pf1mpf  22287  pf1ind  22290  xkofvcn  23619  xpstopnlem1  23744  ufildom1  23861  deg1z  26039  deg1addle  26053  deg1vscale  26056  deg1vsca  26057  deg1mulle2  26061  deg1le0  26063  ply1nzb  26075  sltval2  27615  noextendlt  27628  sltsolem1  27634  nosepnelem  27638  nolt02o  27654  old1  27840  rankeq1o  36287  ssoninhaus  36564  onint1  36565  1oequni2o  37485  finxp1o  37509  finxpreclem3  37510  finxpreclem4  37511  finxpreclem5  37512  finxpsuclem  37514  pw2f1ocnv  43194  wepwsolem  43199  pwfi2f1o  43253  oaabsb  43451  oaordnr  43453  omnord1  43462  oege1  43463  oaomoencom  43474  omabs2  43489  omcl3g  43491  nadd1suc  43549  om2  43561  oe2  43563  safesnsupfiss  43572  safesnsupfidom1o  43574  safesnsupfilb  43575  1no  43593  nlim2NEW  43600  oa1cl  43604  sn1dom  43683  pr2dom  43684  tr3dom  43685  clsk1indlem4  44201