Theorem 2on 8521

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8508	. 2 ⊢ 2o = suc 1o
2		1on 8519	. . 3 ⊢ 1o ∈ On
3		2oex 8518	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2837	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7830	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2836	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2107  Vcvv 3479  Oncon0 6383  suc csuc 6385  1_oc1o 8500  2_oc2o 8501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-tr 5259  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-ord 6386  df-on 6387  df-suc 6389  df-1o 8507  df-2o 8508

This theorem is referenced by:  ord3  8524  3on  8525  ord2eln012  8536  o2p2e4  8580  oneo  8620  2onn  8681  nneob  8695  en3  9317  infxpenc  10059  infxpenc2  10063  mappwen  10153  pwdjuen  10223  ackbij1lem5  10264  sdom2en01  10343  fin1a2lem4  10444  fin1a2lem6  10446  xpsrnbas  17617  xpsadd  17620  xpsmul  17621  xpsvsca  17623  xpsle  17625  cat1  18143  xpsmnd  18791  xpsgrp  19078  efgval  19736  efgtf  19741  frgpcpbl  19778  frgp0  19779  frgpeccl  19780  frgpadd  19782  frgpmhm  19784  vrgpf  19787  vrgpinv  19788  frgpupf  19792  frgpup1  19794  frgpup2  19795  frgpup3lem  19796  frgpnabllem1  19892  frgpnabllem2  19893  xpsrngd  20177  xpsringd  20330  xpstopnlem1  23818  xpstps  23819  xpstopnlem2  23820  xpsxmetlem  24390  xpsdsval  24392  nofv  27703  sltres  27708  noextendgt  27716  nolesgn2ores  27718  nosepnelem  27725  nosepdmlem  27729  nolt02o  27741  nogt01o  27742  nosupno  27749  nosupbnd1lem3  27756  nosupbnd1  27760  nosupbnd2lem1  27761  nosupbnd2  27762  ssoninhaus  36450  onint1  36451  1oequni2o  37370  finxpreclem4  37396  pw2f1ocnv  43054  frlmpwfi  43115  omnord1  43323  oege2  43325  oenord1  43334  oaomoencom  43335  oenassex  43336  oenass  43337  omabs2  43350  oaltom  43423  omltoe  43425  2no  43455  nlim3  43462  tr3dom  43546  enrelmap  44015