Theorem 1on 8446

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8434	. 2 ⊢ 1o = suc ∅
2		0elon 6387	. . 3 ⊢ ∅ ∈ On
3		1oex 8444	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2825	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7785	. . 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 3447  ∅c0 4296  Oncon0 6332  suc csuc 6334  1_oc1o 8427

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336  df-suc 6338  df-1o 8434

This theorem is referenced by:  2on  8447  nlim2  8454  ord1eln01  8460  ondif2  8466  2oconcl  8467  fnoe  8474  oesuclem  8489  oecl  8501  o1p1e2  8504  om1r  8507  oe1m  8509  omword1  8537  omword2  8538  omlimcl  8542  oneo  8545  oewordi  8555  oelim2  8559  oeoa  8561  oeoe  8563  oeeui  8566  1onn  8604  oaabs2  8613  enpr2dOLD  9021  sucxpdom  9202  en2  9226  oancom  9604  cnfcom3lem  9656  ssttrcl  9668  ttrcltr  9669  dmttrcl  9674  ttrclselem2  9679  pm54.43lem  9953  pm54.43  9954  infxpenc  9971  infxpenc2  9975  undjudom  10121  endjudisj  10122  djuen  10123  dju1p1e2  10127  dju1p1e2ALT  10128  xpdjuen  10133  mapdjuen  10134  djuxpdom  10139  djufi  10140  djuinf  10142  infdju1  10143  pwdju1  10144  pwdjudom  10168  isfin4p1  10268  pwxpndom2  10618  wunex2  10691  wuncval2  10700  tsk2  10718  efgmnvl  19644  frgpnabllem1  19803  dmdprdpr  19981  dprdpr  19982  psr1crng  22071  psr1assa  22072  psr1tos  22073  psr1bas  22075  vr1cl2  22077  ply1lss  22081  ply1subrg  22082  ply1ass23l  22111  ressply1bas2  22112  ressply1add  22114  ressply1mul  22115  ressply1vsca  22116  subrgply1  22117  ply1plusgfvi  22126  psr1ring  22131  psr1lmod  22133  psr1sca  22134  ply1ascl  22144  subrg1ascl  22145  subrg1asclcl  22146  subrgvr1  22147  subrgvr1cl  22148  coe1z  22149  coe1mul2lem1  22153  coe1mul2  22155  coe1tm  22159  evls1val  22207  evls1rhm  22209  evls1sca  22210  evl1val  22216  evl1rhm  22219  evl1sca  22221  evl1var  22223  evls1var  22225  mpfpf1  22238  pf1mpf  22239  pf1ind  22242  xkofvcn  23571  xpstopnlem1  23696  ufildom1  23813  deg1z  25992  deg1addle  26006  deg1vscale  26009  deg1vsca  26010  deg1mulle2  26014  deg1le0  26016  ply1nzb  26028  sltval2  27568  noextendlt  27581  sltsolem1  27587  nosepnelem  27591  nolt02o  27607  old1  27787  rankeq1o  36159  ssoninhaus  36436  onint1  36437  1oequni2o  37356  finxp1o  37380  finxpreclem3  37381  finxpreclem4  37382  finxpreclem5  37383  finxpsuclem  37385  pw2f1ocnv  43026  wepwsolem  43031  pwfi2f1o  43085  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