Theorem 1on 8527

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

Assertion

Ref	Expression
1on	⊢ 1o ∈ On

Proof of Theorem 1on

Step	Hyp	Ref	Expression
1		df-1o 8514	. 2 ⊢ 1o = suc ∅
2		0elon 6444	. . 3 ⊢ ∅ ∈ On
3		1oex 8524	. . . 4 ⊢ 1o ∈ V
4	1, 3	eqeltrri 2861	. . 3 ⊢ suc ∅ ∈ V
5		sucexeloni 7857	. . 3 ⊢ ((∅ ∈ On ∧ suc ∅ ∈ V) → suc ∅ ∈ On)
6	2, 4, 5	mp2an 705	. 2 ⊢ suc ∅ ∈ On
7	1, 6	eqeltri 2860	1 ⊢ 1o ∈ On

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ∅c0 4281  Oncon0 6388  suc csuc 6390  1_oc1o 8507

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-tr 5219  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6391  df-on 6392  df-suc 6394  df-1o 8514

This theorem is used by:  2on  8528  nlim2  8536  ord1eln01  8542  ondif2  8548  2oconcl  8549  fnoe  8556  oesuclem  8571  oecl  8583  o1p1e2  8586  om1r  8589  oe1m  8591  omword1  8619  omword2  8620  omlimcl  8624  oneo  8627  om2  8632  oewordi  8638  oelim2  8642  oeoa  8644  oeoe  8646  oeeui  8649  1onn  8687  oaabs2  8696  sucxpdom  9290  en2  9309  oancom  9689  cnfcom3lem  9741  ssttrcl  9753  ttrcltr  9754  dmttrcl  9759  ttrclselem2  9764  pm54.43lem  10120  pm54.43  10121  infxpenc  10136  infxpenc2  10140  undjudom  10285  endjudisj  10286  djuen  10287  dju1p1e2  10291  dju1p1e2ALT  10292  xpdjuen  10297  mapdjuen  10298  djuxpdom  10303  djufi  10304  djuinf  10306  infdju1  10307  pwdju1  10308  pwdjudom  10332  isfin4p1  10432  pwxpndom2  10789  wunex2  10862  wuncval2  10871  tsk2  10889  efgmnvl  19979  frgpnabllem1  20138  dmdprdpr  20316  dprdpr  20317  psr1crng  22560  psr1assa  22561  psr1tos  22562  psr1bas  22564  vr1cl2  22566  ply1lss  22569  ply1subrg  22570  ply1ass23l  22599  ressply1bas2  22600  ressply1add  22602  ressply1mul  22603  ressply1vsca  22604  subrgply1  22605  ply1plusgfvi  22614  psr1ring  22619  psr1lmod  22621  psr1sca  22622  ply1ascl  22632  subrg1ascl  22633  subrg1asclcl  22634  subrgvr1  22635  subrgvr1cl  22636  coe1z  22637  coe1mul2lem1  22641  coe1mul2  22643  coe1tm  22647  evls1val  22693  evls1rhm  22695  evls1sca  22696  evl1val  22702  evl1rhm  22705  evl1sca  22707  evl1var  22709  evls1var  22711  mpfpf1  22724  pf1mpf  22725  pf1ind  22728  xkofvcn  24058  xpstopnlem1  24183  ufildom1  24300  deg1z  26460  deg1addle  26474  deg1vscale  26477  deg1vsca  26478  deg1mulle2  26482  deg1le0  26484  ply1nzb  26496  ltsval2  28070  noextendlt  28083  ltssolem1  28089  nosepnelem  28093  nolt02o  28109  old1  28308  unidifsnel  33229  unidifsnne  33230  1olt9o  35921  gdlopcfv2  36014  gdlopcfv3  36015  gdlopcfv4  36016  gdlopcfv5  36017  gdlopcfv6  36018  gdlopcfv7  36019  gdlopcfv8  36020  rankeq1o  37147  nmulrid  37161  nmullid  37162  ssoninhaus  37451  onint1  37452  1oequni2o  38559  finxp1o  38583  finxpreclem3  38584  finxpreclem4  38585  finxpreclem5  38586  finxpsuclem  38588  pw2f1ocnv  44310  wepwsolem  44315  pwfi2f1o  44364  oaabsb  44557  oaordnr  44559  omnord1  44568  oege1  44569  oaomoencom  44580  omabs2  44595  omcl3g  44597  nadd1suc  44655  oe2  44668  safesnsupfiss  44677  safesnsupfidom1o  44679  safesnsupfilb  44680  1fno  44698  nlim2NEW  44705  oa1cl  44709  sn1dom  44788  pr2dom  44789  tr3dom  44790  clsk1indlem4  45305  setc1onsubc  51071