Theorem 1on 8534

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8522	. 2 ⊢ 1o = suc ∅
2		0elon 6449	. . 3 ⊢ ∅ ∈ On
3		1oex 8532	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2841	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7845	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 691	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2840	1 ⊢ 1o ∈ On

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ∅c0 4352  Oncon0 6395  suc csuc 6397  1_oc1o 8515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399  df-suc 6401  df-1o 8522

This theorem is referenced by:  2on  8536  2onOLD  8537  1oexOLD  8542  nlim2  8546  ord1eln01  8552  ondif2  8558  2oconcl  8559  fnoe  8566  oesuclem  8581  oecl  8593  o1p1e2  8596  om1r  8599  oe1m  8601  omword1  8629  omword2  8630  omlimcl  8634  oneo  8637  oewordi  8647  oelim2  8651  oeoa  8653  oeoe  8655  oeeui  8658  1onn  8696  oaabs2  8705  enpr2dOLD  9116  sucxpdom  9318  en2  9343  oancom  9720  cnfcom3lem  9772  ssttrcl  9784  ttrcltr  9785  dmttrcl  9790  ttrclselem2  9795  pm54.43lem  10069  pm54.43  10070  infxpenc  10087  infxpenc2  10091  undjudom  10237  endjudisj  10238  djuen  10239  dju1p1e2  10243  dju1p1e2ALT  10244  xpdjuen  10249  mapdjuen  10250  djuxpdom  10255  djufi  10256  djuinf  10258  infdju1  10259  pwdju1  10260  pwdjudom  10284  isfin4p1  10384  pwxpndom2  10734  wunex2  10807  wuncval2  10816  tsk2  10834  efgmnvl  19756  frgpnabllem1  19915  dmdprdpr  20093  dprdpr  20094  psr1crng  22209  psr1assa  22210  psr1tos  22211  psr1bas  22213  vr1cl2  22215  ply1lss  22219  ply1subrg  22220  ply1ass23l  22249  ressply1bas2  22250  ressply1add  22252  ressply1mul  22253  ressply1vsca  22254  subrgply1  22255  ply1plusgfvi  22264  psr1ring  22269  psr1lmod  22271  psr1sca  22272  ply1ascl  22282  subrg1ascl  22283  subrg1asclcl  22284  subrgvr1  22285  subrgvr1cl  22286  coe1z  22287  coe1mul2lem1  22291  coe1mul2  22293  coe1tm  22297  evls1val  22345  evls1rhm  22347  evls1sca  22348  evl1val  22354  evl1rhm  22357  evl1sca  22359  evl1var  22361  evls1var  22363  mpfpf1  22376  pf1mpf  22377  pf1ind  22380  xkofvcn  23713  xpstopnlem1  23838  ufildom1  23955  deg1z  26146  deg1addle  26160  deg1vscale  26163  deg1vsca  26164  deg1mulle2  26168  deg1le0  26170  ply1nzb  26182  sltval2  27719  noextendlt  27732  sltsolem1  27738  nosepnelem  27742  nolt02o  27758  old1  27932  rankeq1o  36135  ssoninhaus  36414  onint1  36415  1oequni2o  37334  finxp1o  37358  finxpreclem3  37359  finxpreclem4  37360  finxpreclem5  37361  finxpsuclem  37363  pw2f1ocnv  42994  wepwsolem  42999  pwfi2f1o  43053  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