Theorem 2on 8404

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8392	. 2 ⊢ 2o = suc 1o
2		1on 8403	. . 3 ⊢ 1o ∈ On
3		2oex 8402	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2830	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7748	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2829	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2113  Vcvv 3437  Oncon0 6311  suc csuc 6313  1_oc1o 8384  2_oc2o 8385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-tr 5201  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6314  df-on 6315  df-suc 6317  df-1o 8391  df-2o 8392

This theorem is referenced by:  ord3  8406  3on  8407  ord2eln012  8418  o2p2e4  8462  oneo  8502  2onn  8563  nneob  8577  en3  9172  infxpenc  9916  infxpenc2  9920  mappwen  10010  pwdjuen  10080  ackbij1lem5  10121  sdom2en01  10200  fin1a2lem4  10301  fin1a2lem6  10303  xpsrnbas  17477  xpsadd  17480  xpsmul  17481  xpsvsca  17483  xpsle  17485  cat1  18006  xpsmnd  18687  xpsgrp  18974  efgval  19631  efgtf  19636  frgpcpbl  19673  frgp0  19674  frgpeccl  19675  frgpadd  19677  frgpmhm  19679  vrgpf  19682  vrgpinv  19683  frgpupf  19687  frgpup1  19689  frgpup2  19690  frgpup3lem  19691  frgpnabllem1  19787  frgpnabllem2  19788  xpsrngd  20099  xpsringd  20252  xpstopnlem1  23725  xpstps  23726  xpstopnlem2  23727  xpsxmetlem  24295  xpsdsval  24297  nofv  27597  sltres  27602  noextendgt  27610  nolesgn2ores  27612  nosepnelem  27619  nosepdmlem  27623  nolt02o  27635  nogt01o  27636  nosupno  27643  nosupbnd1lem3  27650  nosupbnd1  27654  nosupbnd2lem1  27655  nosupbnd2  27656  ssoninhaus  36513  onint1  36514  1oequni2o  37433  finxpreclem4  37459  pw2f1ocnv  43155  frlmpwfi  43216  omnord1  43423  oege2  43425  oenord1  43434  oaomoencom  43435  oenassex  43436  oenass  43437  omabs2  43450  oaltom  43523  omltoe  43525  2no  43555  nlim3  43562  tr3dom  43646  enrelmap  44115  nelsubc3  49197