Theorem 1on 8407

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8395	. 2 ⊢ 1o = suc ∅
2		0elon 6365	. . 3 ⊢ ∅ ∈ On
3		1oex 8405	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2836	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7752	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 698	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2835	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2119  Vcvv 3431  ∅c0 4261  Oncon0 6310  suc csuc 6312  1_oc1o 8388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-tr 5180  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-ord 6313  df-on 6314  df-suc 6316  df-1o 8395

This theorem is referenced by:  2on  8408  nlim2  8415  ord1eln01  8421  ondif2  8427  2oconcl  8428  fnoe  8435  oesuclem  8450  oecl  8462  o1p1e2  8465  om1r  8468  oe1m  8470  omword1  8498  omword2  8499  omlimcl  8503  oneo  8506  om2  8511  oewordi  8517  oelim2  8521  oeoa  8523  oeoe  8525  oeeui  8528  1onn  8566  oaabs2  8575  sucxpdom  9161  en2  9180  oancom  9563  cnfcom3lem  9615  ssttrcl  9627  ttrcltr  9628  dmttrcl  9633  ttrclselem2  9638  pm54.43lem  9915  pm54.43  9916  infxpenc  9931  infxpenc2  9935  undjudom  10081  endjudisj  10082  djuen  10083  dju1p1e2  10087  dju1p1e2ALT  10088  xpdjuen  10093  mapdjuen  10094  djuxpdom  10099  djufi  10100  djuinf  10102  infdju1  10103  pwdju1  10104  pwdjudom  10128  isfin4p1  10228  pwxpndom2  10579  wunex2  10652  wuncval2  10661  tsk2  10679  efgmnvl  19680  frgpnabllem1  19839  dmdprdpr  20017  dprdpr  20018  psr1crng  22172  psr1assa  22173  psr1tos  22174  psr1bas  22176  vr1cl2  22178  ply1lss  22181  ply1subrg  22182  ply1ass23l  22211  ressply1bas2  22212  ressply1add  22214  ressply1mul  22215  ressply1vsca  22216  subrgply1  22217  ply1plusgfvi  22226  psr1ring  22231  psr1lmod  22233  psr1sca  22234  ply1ascl  22244  subrg1ascl  22245  subrg1asclcl  22246  subrgvr1  22247  subrgvr1cl  22248  coe1z  22249  coe1mul2lem1  22253  coe1mul2  22255  coe1tm  22259  evls1val  22306  evls1rhm  22308  evls1sca  22309  evl1val  22315  evl1rhm  22318  evl1sca  22320  evl1var  22322  evls1var  22324  mpfpf1  22337  pf1mpf  22338  pf1ind  22341  xkofvcn  23667  xpstopnlem1  23792  ufildom1  23909  deg1z  26070  deg1addle  26084  deg1vscale  26087  deg1vsca  26088  deg1mulle2  26092  deg1le0  26094  ply1nzb  26106  ltsval2  27638  noextendlt  27651  ltssolem1  27657  nosepnelem  27661  nolt02o  27677  old1  27875  rankeq1o  36399  ssoninhaus  36676  onint1  36677  1oequni2o  37730  finxp1o  37754  finxpreclem3  37755  finxpreclem4  37756  finxpreclem5  37757  finxpsuclem  37759  pw2f1ocnv  43482  wepwsolem  43487  pwfi2f1o  43541  oaabsb  43739  oaordnr  43741  omnord1  43750  oege1  43751  oaomoencom  43762  omabs2  43777  omcl3g  43779  nadd1suc  43837  oe2  43850  safesnsupfiss  43859  safesnsupfidom1o  43861  safesnsupfilb  43862  1fno  43880  nlim2NEW  43887  oa1cl  43891  sn1dom  43970  pr2dom  43971  tr3dom  43972  clsk1indlem4  44488  setc1onsubc  50092