Theorem 2on 8408

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8396	. 2 ⊢ 2o = suc 1o
2		1on 8407	. . 3 ⊢ 1o ∈ On
3		2oex 8406	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2825	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7749	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2824	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2109  Vcvv 3438  Oncon0 6311  suc csuc 6313  1_oc1o 8388  2_oc2o 8389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-ord 6314  df-on 6315  df-suc 6317  df-1o 8395  df-2o 8396

This theorem is referenced by:  ord3  8410  3on  8411  ord2eln012  8422  o2p2e4  8466  oneo  8506  2onn  8567  nneob  8581  en3  9185  infxpenc  9931  infxpenc2  9935  mappwen  10025  pwdjuen  10095  ackbij1lem5  10136  sdom2en01  10215  fin1a2lem4  10316  fin1a2lem6  10318  xpsrnbas  17493  xpsadd  17496  xpsmul  17497  xpsvsca  17499  xpsle  17501  cat1  18022  xpsmnd  18669  xpsgrp  18956  efgval  19614  efgtf  19619  frgpcpbl  19656  frgp0  19657  frgpeccl  19658  frgpadd  19660  frgpmhm  19662  vrgpf  19665  vrgpinv  19666  frgpupf  19670  frgpup1  19672  frgpup2  19673  frgpup3lem  19674  frgpnabllem1  19770  frgpnabllem2  19771  xpsrngd  20082  xpsringd  20235  xpstopnlem1  23712  xpstps  23713  xpstopnlem2  23714  xpsxmetlem  24283  xpsdsval  24285  nofv  27585  sltres  27590  noextendgt  27598  nolesgn2ores  27600  nosepnelem  27607  nosepdmlem  27611  nolt02o  27623  nogt01o  27624  nosupno  27631  nosupbnd1lem3  27638  nosupbnd1  27642  nosupbnd2lem1  27643  nosupbnd2  27644  ssoninhaus  36421  onint1  36422  1oequni2o  37341  finxpreclem4  37367  pw2f1ocnv  43010  frlmpwfi  43071  omnord1  43278  oege2  43280  oenord1  43289  oaomoencom  43290  oenassex  43291  oenass  43292  omabs2  43305  oaltom  43378  omltoe  43380  2no  43410  nlim3  43417  tr3dom  43501  enrelmap  43970  nelsubc3  49057