Theorem 2on 8499

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8486	. 2 ⊢ 2o = suc 1o
2		1on 8497	. . 3 ⊢ 1o ∈ On
3		2oex 8496	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2832	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7808	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2831	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2109  Vcvv 3464  Oncon0 6357  suc csuc 6359  1_oc1o 8478  2_oc2o 8479

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-tr 5235  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6360  df-on 6361  df-suc 6363  df-1o 8485  df-2o 8486

This theorem is referenced by:  ord3  8502  3on  8503  ord2eln012  8514  o2p2e4  8558  oneo  8598  2onn  8659  nneob  8673  en3  9293  infxpenc  10037  infxpenc2  10041  mappwen  10131  pwdjuen  10201  ackbij1lem5  10242  sdom2en01  10321  fin1a2lem4  10422  fin1a2lem6  10424  xpsrnbas  17590  xpsadd  17593  xpsmul  17594  xpsvsca  17596  xpsle  17598  cat1  18115  xpsmnd  18760  xpsgrp  19047  efgval  19703  efgtf  19708  frgpcpbl  19745  frgp0  19746  frgpeccl  19747  frgpadd  19749  frgpmhm  19751  vrgpf  19754  vrgpinv  19755  frgpupf  19759  frgpup1  19761  frgpup2  19762  frgpup3lem  19763  frgpnabllem1  19859  frgpnabllem2  19860  xpsrngd  20144  xpsringd  20297  xpstopnlem1  23752  xpstps  23753  xpstopnlem2  23754  xpsxmetlem  24323  xpsdsval  24325  nofv  27626  sltres  27631  noextendgt  27639  nolesgn2ores  27641  nosepnelem  27648  nosepdmlem  27652  nolt02o  27664  nogt01o  27665  nosupno  27672  nosupbnd1lem3  27679  nosupbnd1  27683  nosupbnd2lem1  27684  nosupbnd2  27685  ssoninhaus  36471  onint1  36472  1oequni2o  37391  finxpreclem4  37417  pw2f1ocnv  43028  frlmpwfi  43089  omnord1  43296  oege2  43298  oenord1  43307  oaomoencom  43308  oenassex  43309  oenass  43310  omabs2  43323  oaltom  43396  omltoe  43398  2no  43428  nlim3  43435  tr3dom  43519  enrelmap  43988  nelsubc3  49005