Theorem 1on 8482

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8469	. 2 ⊢ 1o = suc ∅
2		0elon 6417	. . 3 ⊢ ∅ ∈ On
3		1oex 8479	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2858	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7821	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 705	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2857	1 ⊢ 1o ∈ On

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ∅c0 4279  Oncon0 6361  suc csuc 6363  1_oc1o 8462

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6364  df-on 6365  df-suc 6367  df-1o 8469

This theorem is used by:  2on  8483  nlim2  8491  ord1eln01  8497  ondif2  8503  2oconcl  8504  fnoe  8511  oesuclem  8526  oecl  8538  o1p1e2  8541  om1r  8544  oe1m  8546  omword1  8574  omword2  8575  omlimcl  8579  oneo  8582  om2  8587  oewordi  8593  oelim2  8597  oeoa  8599  oeoe  8601  oeeui  8604  1onn  8642  oaabs2  8651  sucxpdom  9245  en2  9264  oancom  9645  cnfcom3lem  9697  ssttrcl  9709  ttrcltr  9710  dmttrcl  9715  ttrclselem2  9720  pm54.43lem  10074  pm54.43  10075  infxpenc  10090  infxpenc2  10094  undjudom  10239  endjudisj  10240  djuen  10241  dju1p1e2  10245  dju1p1e2ALT  10246  xpdjuen  10251  mapdjuen  10252  djuxpdom  10257  djufi  10258  djuinf  10260  infdju1  10261  pwdju1  10262  pwdjudom  10286  isfin4p1  10386  pwxpndom2  10743  wunex2  10816  wuncval2  10825  tsk2  10843  efgmnvl  19921  frgpnabllem1  20080  dmdprdpr  20258  dprdpr  20259  psr1crng  22498  psr1assa  22499  psr1tos  22500  psr1bas  22502  vr1cl2  22504  ply1lss  22507  ply1subrg  22508  ply1ass23l  22537  ressply1bas2  22538  ressply1add  22540  ressply1mul  22541  ressply1vsca  22542  subrgply1  22543  ply1plusgfvi  22552  psr1ring  22557  psr1lmod  22559  psr1sca  22560  ply1ascl  22570  subrg1ascl  22571  subrg1asclcl  22572  subrgvr1  22573  subrgvr1cl  22574  coe1z  22575  coe1mul2lem1  22579  coe1mul2  22581  coe1tm  22585  evls1val  22631  evls1rhm  22633  evls1sca  22634  evl1val  22640  evl1rhm  22643  evl1sca  22645  evl1var  22647  evls1var  22649  mpfpf1  22662  pf1mpf  22663  pf1ind  22666  xkofvcn  23996  xpstopnlem1  24121  ufildom1  24238  deg1z  26398  deg1addle  26412  deg1vscale  26415  deg1vsca  26416  deg1mulle2  26420  deg1le0  26422  ply1nzb  26434  ltsval2  28006  noextendlt  28019  ltssolem1  28025  nosepnelem  28029  nolt02o  28045  old1  28244  rankeq1o  36912  nmulrid  36926  nmullid  36927  ssoninhaus  37216  onint1  37217  1oequni2o  38271  finxp1o  38295  finxpreclem3  38296  finxpreclem4  38297  finxpreclem5  38298  finxpsuclem  38300  pw2f1ocnv  44023  wepwsolem  44028  pwfi2f1o  44082  oaabsb  44280  oaordnr  44282  omnord1  44291  oege1  44292  oaomoencom  44303  omabs2  44318  omcl3g  44320  nadd1suc  44378  oe2  44391  safesnsupfiss  44400  safesnsupfidom1o  44402  safesnsupfilb  44403  1fno  44421  nlim2NEW  44428  oa1cl  44432  sn1dom  44511  pr2dom  44512  tr3dom  44513  clsk1indlem4  45029  setc1onsubc  50679