Theorem 2on 8420

Description: Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) Avoid ax-un 7690. (Revised by BTernaryTau, 30-Nov-2024.)

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8408	. 2 ⊢ 2o = suc 1o
2		1on 8419	. . 3 ⊢ 1o ∈ On
3		2oex 8418	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2834	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7764	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 693	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2833	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2114  Vcvv 3442  Oncon0 6325  suc csuc 6327  1_oc1o 8400  2_oc2o 8401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-on 6329  df-suc 6331  df-1o 8407  df-2o 8408

This theorem is referenced by:  ord3  8422  3on  8423  ord2eln012  8434  o2p2e4  8478  oneo  8518  2onn  8580  nneob  8594  en3  9193  infxpenc  9940  infxpenc2  9944  mappwen  10034  pwdjuen  10104  ackbij1lem5  10145  sdom2en01  10224  fin1a2lem4  10325  fin1a2lem6  10327  xpsrnbas  17504  xpsadd  17507  xpsmul  17508  xpsvsca  17510  xpsle  17512  cat1  18033  xpsmnd  18714  xpsgrp  19001  efgval  19658  efgtf  19663  frgpcpbl  19700  frgp0  19701  frgpeccl  19702  frgpadd  19704  frgpmhm  19706  vrgpf  19709  vrgpinv  19710  frgpupf  19714  frgpup1  19716  frgpup2  19717  frgpup3lem  19718  frgpnabllem1  19814  frgpnabllem2  19815  xpsrngd  20126  xpsringd  20280  xpstopnlem1  23765  xpstps  23766  xpstopnlem2  23767  xpsxmetlem  24335  xpsdsval  24337  nofv  27637  ltsres  27642  noextendgt  27650  nolesgn2ores  27652  nosepnelem  27659  nosepdmlem  27663  nolt02o  27675  nogt01o  27676  nosupno  27683  nosupbnd1lem3  27690  nosupbnd1  27694  nosupbnd2lem1  27695  nosupbnd2  27696  bdaypw2n0bndlem  28471  ssoninhaus  36661  onint1  36662  1oequni2o  37617  finxpreclem4  37643  pw2f1ocnv  43388  frlmpwfi  43449  omnord1  43656  oege2  43658  oenord1  43667  oaomoencom  43668  oenassex  43669  oenass  43670  omabs2  43683  oaltom  43755  omltoe  43757  2fno  43787  nlim3  43794  tr3dom  43878  enrelmap  44347  nelsubc3  49424