Theorem 2on 8415

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8403	. 2 ⊢ 2o = suc 1o
2		1on 8414	. . 3 ⊢ 1o ∈ On
3		2oex 8413	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2837	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7759	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 698	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2836	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2119  Vcvv 3432  Oncon0 6317  suc csuc 6319  1_oc1o 8395  2_oc2o 8396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-tr 5187  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6320  df-on 6321  df-suc 6323  df-1o 8402  df-2o 8403

This theorem is referenced by:  ord3  8417  3on  8418  ord2eln012  8429  o2p2e4  8473  oneo  8513  2onn  8575  nneob  8589  en3  9188  infxpenc  9938  infxpenc2  9942  mappwen  10032  pwdjuen  10102  ackbij1lem5  10143  sdom2en01  10222  fin1a2lem4  10323  fin1a2lem6  10325  xpsrnbas  17533  xpsadd  17536  xpsmul  17537  xpsvsca  17539  xpsle  17541  cat1  18062  xpsmnd  18743  xpsgrp  19033  efgval  19690  efgtf  19695  frgpcpbl  19732  frgp0  19733  frgpeccl  19734  frgpadd  19736  frgpmhm  19738  vrgpf  19741  vrgpinv  19742  frgpupf  19746  frgpup1  19748  frgpup2  19749  frgpup3lem  19750  frgpnabllem1  19846  frgpnabllem2  19847  xpsrngd  20158  xpsringd  20310  xpstopnlem1  23799  xpstps  23800  xpstopnlem2  23801  xpsxmetlem  24369  xpsdsval  24371  nofv  27646  ltsres  27651  noextendgt  27659  nolesgn2ores  27661  nosepnelem  27668  nosepdmlem  27672  nolt02o  27684  nogt01o  27685  nosupno  27692  nosupbnd1lem3  27699  nosupbnd1  27703  nosupbnd2lem1  27704  nosupbnd2  27705  bdaypw2n0bndlem  28480  ssoninhaus  36683  onint1  36684  1oequni2o  37737  finxpreclem4  37763  pw2f1ocnv  43489  frlmpwfi  43550  omnord1  43757  oege2  43759  oenord1  43768  oaomoencom  43769  oenassex  43770  oenass  43771  omabs2  43784  oaltom  43856  omltoe  43858  2fno  43888  nlim3  43895  tr3dom  43979  enrelmap  44448  nelsubc3  49568