Theorem 2on 8446

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8433	. 2 ⊢ 2o = suc 1o
2		1on 8445	. . 3 ⊢ 1o ∈ On
3		2oex 8444	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2858	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7788	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 702	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2857	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2141  Vcvv 3453  Oncon0 6342  suc csuc 6344  1_oc1o 8425  2_oc2o 8426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-tr 5207  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-ord 6345  df-on 6346  df-suc 6348  df-1o 8432  df-2o 8433

This theorem is referenced by:  ord3  8448  3on  8449  ord2eln012  8461  o2p2e4  8505  oneo  8545  2onn  8607  nneob  8621  en3  9221  infxpenc  9971  infxpenc2  9975  mappwen  10065  pwdjuen  10135  ackbij1lem5  10176  sdom2en01  10256  fin1a2lem4  10357  fin1a2lem6  10359  xpsrnbas  17584  xpsadd  17587  xpsmul  17588  xpsvsca  17590  xpsle  17592  cat1  18113  xpsmnd  18794  xpsgrp  19084  efgval  19740  efgtf  19745  frgpcpbl  19782  frgp0  19783  frgpeccl  19784  frgpadd  19786  frgpmhm  19788  vrgpf  19791  vrgpinv  19792  frgpupf  19796  frgpup1  19798  frgpup2  19799  frgpup3lem  19800  frgpnabllem1  19896  frgpnabllem2  19897  xpsrngd  20208  xpsringd  20360  xpstopnlem1  23849  xpstps  23850  xpstopnlem2  23851  xpsxmetlem  24419  xpsdsval  24421  nofv  27698  ltsres  27703  noextendgt  27711  nolesgn2ores  27713  nosepnelem  27720  nosepdmlem  27724  nolt02o  27736  nogt01o  27737  nosupno  27744  nosupbnd1lem3  27751  nosupbnd1  27755  nosupbnd2lem1  27756  nosupbnd2  27757  bdaypw2n0bndlem  28533  ssoninhaus  36772  onint1  36773  1oequni2o  37826  finxpreclem4  37852  pw2f1ocnv  43578  frlmpwfi  43639  omnord1  43846  oege2  43848  oenord1  43857  oaomoencom  43858  oenassex  43859  oenass  43860  omabs2  43873  oaltom  43945  omltoe  43947  2fno  43977  nlim3  43984  tr3dom  44068  enrelmap  44537  nelsubc3  49656