Theorem 2on 8411

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8399	. 2 ⊢ 2o = suc 1o
2		1on 8410	. . 3 ⊢ 1o ∈ On
3		2oex 8409	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2834	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7756	. . 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 3430  Oncon0 6317  suc csuc 6319  1_oc1o 8391  2_oc2o 8392

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 5231  ax-nul 5241  ax-pr 5370

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-suc 6323  df-1o 8398  df-2o 8399

This theorem is referenced by:  ord3  8413  3on  8414  ord2eln012  8425  o2p2e4  8469  oneo  8509  2onn  8571  nneob  8585  en3  9184  infxpenc  9931  infxpenc2  9935  mappwen  10025  pwdjuen  10095  ackbij1lem5  10136  sdom2en01  10215  fin1a2lem4  10316  fin1a2lem6  10318  xpsrnbas  17526  xpsadd  17529  xpsmul  17530  xpsvsca  17532  xpsle  17534  cat1  18055  xpsmnd  18736  xpsgrp  19026  efgval  19683  efgtf  19688  frgpcpbl  19725  frgp0  19726  frgpeccl  19727  frgpadd  19729  frgpmhm  19731  vrgpf  19734  vrgpinv  19735  frgpupf  19739  frgpup1  19741  frgpup2  19742  frgpup3lem  19743  frgpnabllem1  19839  frgpnabllem2  19840  xpsrngd  20151  xpsringd  20303  xpstopnlem1  23784  xpstps  23785  xpstopnlem2  23786  xpsxmetlem  24354  xpsdsval  24356  nofv  27635  ltsres  27640  noextendgt  27648  nolesgn2ores  27650  nosepnelem  27657  nosepdmlem  27661  nolt02o  27673  nogt01o  27674  nosupno  27681  nosupbnd1lem3  27688  nosupbnd1  27692  nosupbnd2lem1  27693  nosupbnd2  27694  bdaypw2n0bndlem  28469  ssoninhaus  36646  onint1  36647  1oequni2o  37698  finxpreclem4  37724  pw2f1ocnv  43483  frlmpwfi  43544  omnord1  43751  oege2  43753  oenord1  43762  oaomoencom  43763  oenassex  43764  oenass  43765  omabs2  43778  oaltom  43850  omltoe  43852  2fno  43882  nlim3  43889  tr3dom  43973  enrelmap  44442  nelsubc3  49558