Theorem 1on 8493

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8480	. 2 ⊢ 1o = suc ∅
2		0elon 6418	. . 3 ⊢ ∅ ∈ On
3		1oex 8490	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2857	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7824	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 705	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2856	1 ⊢ 1o ∈ On

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ∅c0 4278  Oncon0 6362  suc csuc 6364  1_oc1o 8473

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366  df-suc 6368  df-1o 8480

This theorem is used by:  2on  8494  nlim2  8502  ord1eln01  8508  ondif2  8514  2oconcl  8515  fnoe  8522  oesuclem  8537  oecl  8549  o1p1e2  8552  om1r  8555  oe1m  8557  omword1  8585  omword2  8586  omlimcl  8590  oneo  8593  om2  8598  oewordi  8604  oelim2  8608  oeoa  8610  oeoe  8612  oeeui  8615  1onn  8653  oaabs2  8662  sucxpdom  9256  en2  9275  oancom  9656  cnfcom3lem  9708  ssttrcl  9720  ttrcltr  9721  dmttrcl  9726  ttrclselem2  9731  pm54.43lem  10085  pm54.43  10086  infxpenc  10101  infxpenc2  10105  undjudom  10250  endjudisj  10251  djuen  10252  dju1p1e2  10256  dju1p1e2ALT  10257  xpdjuen  10262  mapdjuen  10263  djuxpdom  10268  djufi  10269  djuinf  10271  infdju1  10272  pwdju1  10273  pwdjudom  10297  isfin4p1  10397  pwxpndom2  10754  wunex2  10827  wuncval2  10836  tsk2  10854  efgmnvl  19934  frgpnabllem1  20093  dmdprdpr  20271  dprdpr  20272  psr1crng  22511  psr1assa  22512  psr1tos  22513  psr1bas  22515  vr1cl2  22517  ply1lss  22520  ply1subrg  22521  ply1ass23l  22550  ressply1bas2  22551  ressply1add  22553  ressply1mul  22554  ressply1vsca  22555  subrgply1  22556  ply1plusgfvi  22565  psr1ring  22570  psr1lmod  22572  psr1sca  22573  ply1ascl  22583  subrg1ascl  22584  subrg1asclcl  22585  subrgvr1  22586  subrgvr1cl  22587  coe1z  22588  coe1mul2lem1  22592  coe1mul2  22594  coe1tm  22598  evls1val  22644  evls1rhm  22646  evls1sca  22647  evl1val  22653  evl1rhm  22656  evl1sca  22658  evl1var  22660  evls1var  22662  mpfpf1  22675  pf1mpf  22676  pf1ind  22679  xkofvcn  24009  xpstopnlem1  24134  ufildom1  24251  deg1z  26411  deg1addle  26425  deg1vscale  26428  deg1vsca  26429  deg1mulle2  26433  deg1le0  26435  ply1nzb  26447  ltsval2  28019  noextendlt  28032  ltssolem1  28038  nosepnelem  28042  nolt02o  28058  old1  28257  unidifsnel  33179  unidifsnne  33180  rankeq1o  37025  nmulrid  37039  nmullid  37040  ssoninhaus  37329  onint1  37330  1oequni2o  38385  finxp1o  38409  finxpreclem3  38410  finxpreclem4  38411  finxpreclem5  38412  finxpsuclem  38414  pw2f1ocnv  44138  wepwsolem  44143  pwfi2f1o  44192  oaabsb  44390  oaordnr  44392  omnord1  44401  oege1  44402  oaomoencom  44413  omabs2  44428  omcl3g  44430  nadd1suc  44488  oe2  44501  safesnsupfiss  44510  safesnsupfidom1o  44512  safesnsupfilb  44513  1fno  44531  nlim2NEW  44538  oa1cl  44542  sn1dom  44621  pr2dom  44622  tr3dom  44623  clsk1indlem4  45138  setc1onsubc  50834