Theorem 2on 8455

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8442	. 2 ⊢ 2o = suc 1o
2		1on 8454	. . 3 ⊢ 1o ∈ On
3		2oex 8453	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2862	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7796	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 704	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2861	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2145  Vcvv 3457  Oncon0 6350  suc csuc 6352  1_oc1o 8434  2_oc2o 8435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-tr 5213  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-ord 6353  df-on 6354  df-suc 6356  df-1o 8441  df-2o 8442

This theorem is referenced by:  ord3  8457  3on  8458  ord2eln012  8470  o2p2e4  8514  oneo  8554  2onn  8616  nneob  8630  en3  9229  infxpenc  9990  infxpenc2  9994  mappwen  10084  pwdjuen  10153  ackbij1lem5  10194  sdom2en01  10274  fin1a2lem4  10375  fin1a2lem6  10377  xpsrnbas  17615  xpsadd  17618  xpsmul  17619  xpsvsca  17621  xpsle  17623  cat1  18144  xpsmnd  18825  xpsgrp  19116  efgval  19778  efgtf  19783  frgpcpbl  19820  frgp0  19821  frgpeccl  19822  frgpadd  19824  frgpmhm  19826  vrgpf  19829  vrgpinv  19830  frgpupf  19834  frgpup1  19836  frgpup2  19837  frgpup3lem  19838  frgpnabllem1  19934  frgpnabllem2  19935  xpsrngd  20248  xpsringd  20405  xpstopnlem1  23927  xpstps  23928  xpstopnlem2  23929  xpsxmetlem  24497  xpsdsval  24499  nofv  27779  ltsres  27784  noextendgt  27792  nolesgn2ores  27794  nosepnelem  27801  nosepdmlem  27805  nolt02o  27817  nogt01o  27818  nosupno  27825  nosupbnd1lem3  27832  nosupbnd1  27836  nosupbnd2lem1  27837  nosupbnd2  27838  bdaypw2n0bndlem  28614  ssoninhaus  36821  onint1  36822  1oequni2o  37874  finxpreclem4  37900  pw2f1ocnv  43626  frlmpwfi  43687  omnord1  43894  oege2  43896  oenord1  43905  oaomoencom  43906  oenassex  43907  oenass  43908  omabs2  43921  oaltom  43993  omltoe  43995  2fno  44025  nlim3  44032  tr3dom  44116  enrelmap  44585  nelsubc3  49700