Theorem 2on 8410

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8398	. 2 ⊢ 2o = suc 1o
2		1on 8409	. . 3 ⊢ 1o ∈ On
3		2oex 8408	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2833	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7754	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2832	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2113  Vcvv 3440  Oncon0 6317  suc csuc 6319  1_oc1o 8390  2_oc2o 8391

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 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-tr 5206  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 8397  df-2o 8398

This theorem is referenced by:  ord3  8412  3on  8413  ord2eln012  8424  o2p2e4  8468  oneo  8508  2onn  8570  nneob  8584  en3  9181  infxpenc  9928  infxpenc2  9932  mappwen  10022  pwdjuen  10092  ackbij1lem5  10133  sdom2en01  10212  fin1a2lem4  10313  fin1a2lem6  10315  xpsrnbas  17492  xpsadd  17495  xpsmul  17496  xpsvsca  17498  xpsle  17500  cat1  18021  xpsmnd  18702  xpsgrp  18989  efgval  19646  efgtf  19651  frgpcpbl  19688  frgp0  19689  frgpeccl  19690  frgpadd  19692  frgpmhm  19694  vrgpf  19697  vrgpinv  19698  frgpupf  19702  frgpup1  19704  frgpup2  19705  frgpup3lem  19706  frgpnabllem1  19802  frgpnabllem2  19803  xpsrngd  20114  xpsringd  20268  xpstopnlem1  23753  xpstps  23754  xpstopnlem2  23755  xpsxmetlem  24323  xpsdsval  24325  nofv  27625  ltsres  27630  noextendgt  27638  nolesgn2ores  27640  nosepnelem  27647  nosepdmlem  27651  nolt02o  27663  nogt01o  27664  nosupno  27671  nosupbnd1lem3  27678  nosupbnd1  27682  nosupbnd2lem1  27683  nosupbnd2  27684  bdaypw2n0bndlem  28459  ssoninhaus  36642  onint1  36643  1oequni2o  37569  finxpreclem4  37595  pw2f1ocnv  43275  frlmpwfi  43336  omnord1  43543  oege2  43545  oenord1  43554  oaomoencom  43555  oenassex  43556  oenass  43557  omabs2  43570  oaltom  43642  omltoe  43644  2fno  43674  nlim3  43681  tr3dom  43765  enrelmap  44234  nelsubc3  49312