Theorem 2on 8418

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8406	. 2 ⊢ 2o = suc 1o
2		1on 8417	. . 3 ⊢ 1o ∈ On
3		2oex 8416	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2833	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7763	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 693	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2832	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2114  Vcvv 3429  Oncon0 6323  suc csuc 6325  1_oc1o 8398  2_oc2o 8399

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-tr 5193  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6326  df-on 6327  df-suc 6329  df-1o 8405  df-2o 8406

This theorem is referenced by:  ord3  8420  3on  8421  ord2eln012  8432  o2p2e4  8476  oneo  8516  2onn  8578  nneob  8592  en3  9191  infxpenc  9940  infxpenc2  9944  mappwen  10034  pwdjuen  10104  ackbij1lem5  10145  sdom2en01  10224  fin1a2lem4  10325  fin1a2lem6  10327  xpsrnbas  17535  xpsadd  17538  xpsmul  17539  xpsvsca  17541  xpsle  17543  cat1  18064  xpsmnd  18745  xpsgrp  19035  efgval  19692  efgtf  19697  frgpcpbl  19734  frgp0  19735  frgpeccl  19736  frgpadd  19738  frgpmhm  19740  vrgpf  19743  vrgpinv  19744  frgpupf  19748  frgpup1  19750  frgpup2  19751  frgpup3lem  19752  frgpnabllem1  19848  frgpnabllem2  19849  xpsrngd  20160  xpsringd  20312  xpstopnlem1  23774  xpstps  23775  xpstopnlem2  23776  xpsxmetlem  24344  xpsdsval  24346  nofv  27621  ltsres  27626  noextendgt  27634  nolesgn2ores  27636  nosepnelem  27643  nosepdmlem  27647  nolt02o  27659  nogt01o  27660  nosupno  27667  nosupbnd1lem3  27674  nosupbnd1  27678  nosupbnd2lem1  27679  nosupbnd2  27680  bdaypw2n0bndlem  28455  ssoninhaus  36630  onint1  36631  1oequni2o  37684  finxpreclem4  37710  pw2f1ocnv  43465  frlmpwfi  43526  omnord1  43733  oege2  43735  oenord1  43744  oaomoencom  43745  oenassex  43746  oenass  43747  omabs2  43760  oaltom  43832  omltoe  43834  2fno  43864  nlim3  43871  tr3dom  43955  enrelmap  44424  nelsubc3  49546