Theorem 1on 8423

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8411	. 2 ⊢ 1o = suc ∅
2		0elon 6375	. . 3 ⊢ ∅ ∈ On
3		1oex 8421	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2825	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7765	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2824	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ∅c0 4292  Oncon0 6320  suc csuc 6322  1_oc1o 8404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-tr 5210  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6323  df-on 6324  df-suc 6326  df-1o 8411

This theorem is referenced by:  2on  8424  nlim2  8431  ord1eln01  8437  ondif2  8443  2oconcl  8444  fnoe  8451  oesuclem  8466  oecl  8478  o1p1e2  8481  om1r  8484  oe1m  8486  omword1  8514  omword2  8515  omlimcl  8519  oneo  8522  oewordi  8532  oelim2  8536  oeoa  8538  oeoe  8540  oeeui  8543  1onn  8581  oaabs2  8590  enpr2dOLD  8998  sucxpdom  9178  en2  9202  oancom  9580  cnfcom3lem  9632  ssttrcl  9644  ttrcltr  9645  dmttrcl  9650  ttrclselem2  9655  pm54.43lem  9929  pm54.43  9930  infxpenc  9947  infxpenc2  9951  undjudom  10097  endjudisj  10098  djuen  10099  dju1p1e2  10103  dju1p1e2ALT  10104  xpdjuen  10109  mapdjuen  10110  djuxpdom  10115  djufi  10116  djuinf  10118  infdju1  10119  pwdju1  10120  pwdjudom  10144  isfin4p1  10244  pwxpndom2  10594  wunex2  10667  wuncval2  10676  tsk2  10694  efgmnvl  19620  frgpnabllem1  19779  dmdprdpr  19957  dprdpr  19958  psr1crng  22047  psr1assa  22048  psr1tos  22049  psr1bas  22051  vr1cl2  22053  ply1lss  22057  ply1subrg  22058  ply1ass23l  22087  ressply1bas2  22088  ressply1add  22090  ressply1mul  22091  ressply1vsca  22092  subrgply1  22093  ply1plusgfvi  22102  psr1ring  22107  psr1lmod  22109  psr1sca  22110  ply1ascl  22120  subrg1ascl  22121  subrg1asclcl  22122  subrgvr1  22123  subrgvr1cl  22124  coe1z  22125  coe1mul2lem1  22129  coe1mul2  22131  coe1tm  22135  evls1val  22183  evls1rhm  22185  evls1sca  22186  evl1val  22192  evl1rhm  22195  evl1sca  22197  evl1var  22199  evls1var  22201  mpfpf1  22214  pf1mpf  22215  pf1ind  22218  xkofvcn  23547  xpstopnlem1  23672  ufildom1  23789  deg1z  25968  deg1addle  25982  deg1vscale  25985  deg1vsca  25986  deg1mulle2  25990  deg1le0  25992  ply1nzb  26004  sltval2  27544  noextendlt  27557  sltsolem1  27563  nosepnelem  27567  nolt02o  27583  old1  27763  rankeq1o  36132  ssoninhaus  36409  onint1  36410  1oequni2o  37329  finxp1o  37353  finxpreclem3  37354  finxpreclem4  37355  finxpreclem5  37356  finxpsuclem  37358  pw2f1ocnv  42999  wepwsolem  43004  pwfi2f1o  43058  oaabsb  43256  oaordnr  43258  omnord1  43267  oege1  43268  oaomoencom  43279  omabs2  43294  omcl3g  43296  nadd1suc  43354  om2  43366  oe2  43368  safesnsupfiss  43377  safesnsupfidom1o  43379  safesnsupfilb  43380  1no  43398  nlim2NEW  43405  oa1cl  43409  sn1dom  43488  pr2dom  43489  tr3dom  43490  clsk1indlem4  44006