Theorem 2on 8462

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8449	. 2 ⊢ 2o = suc 1o
2		1on 8460	. . 3 ⊢ 1o ∈ On
3		2oex 8459	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2829	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7780	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 690	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2828	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2106  Vcvv 3473  Oncon0 6353  suc csuc 6355  1_oc1o 8441  2_oc2o 8442

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-opab 5204  df-tr 5259  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-ord 6356  df-on 6357  df-suc 6359  df-1o 8448  df-2o 8449

This theorem is referenced by:  ord3  8465  3on  8466  ord2eln012  8479  o2p2e4  8523  o2p2e4OLD  8524  oneo  8564  2onn  8624  nneob  8638  en3  9265  infxpenc  9995  infxpenc2  9999  mappwen  10089  pwdjuen  10158  ackbij1lem5  10201  sdom2en01  10279  fin1a2lem4  10380  fin1a2lem6  10382  xpsrnbas  17499  xpsadd  17502  xpsmul  17503  xpsvsca  17505  xpsle  17507  cat1  18029  xpsmnd  18642  xpsgrp  18916  efgval  19549  efgtf  19554  frgpcpbl  19591  frgp0  19592  frgpeccl  19593  frgpadd  19595  frgpmhm  19597  vrgpf  19600  vrgpinv  19601  frgpupf  19605  frgpup1  19607  frgpup2  19608  frgpup3lem  19609  frgpnabllem1  19701  frgpnabllem2  19702  xpstopnlem1  23242  xpstps  23243  xpstopnlem2  23244  xpsxmetlem  23814  xpsdsval  23816  nofv  27087  sltres  27092  noextendgt  27100  nolesgn2ores  27102  nosepnelem  27109  nosepdmlem  27113  nolt02o  27125  nogt01o  27126  nosupno  27133  nosupbnd1lem3  27140  nosupbnd1  27144  nosupbnd2lem1  27145  nosupbnd2  27146  ssoninhaus  35137  onint1  35138  1oequni2o  36053  finxpreclem4  36079  pw2f1ocnv  41547  frlmpwfi  41611  omnord1  41826  oege2  41828  oenord1  41837  oaomoencom  41838  oenassex  41839  oenass  41840  omabs2  41853  oaltom  41927  omltoe  41929  2no  41959  nlim3  41966  tr3dom  42050  enrelmap  42519