Theorem 2on 8398

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8386	. 2 ⊢ 2o = suc 1o
2		1on 8397	. . 3 ⊢ 1o ∈ On
3		2oex 8396	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2828	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7742	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2827	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2111  Vcvv 3436  Oncon0 6306  suc csuc 6308  1_oc1o 8378  2_oc2o 8379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-tr 5199  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-ord 6309  df-on 6310  df-suc 6312  df-1o 8385  df-2o 8386

This theorem is referenced by:  ord3  8400  3on  8401  ord2eln012  8412  o2p2e4  8456  oneo  8496  2onn  8557  nneob  8571  en3  9165  infxpenc  9909  infxpenc2  9913  mappwen  10003  pwdjuen  10073  ackbij1lem5  10114  sdom2en01  10193  fin1a2lem4  10294  fin1a2lem6  10296  xpsrnbas  17475  xpsadd  17478  xpsmul  17479  xpsvsca  17481  xpsle  17483  cat1  18004  xpsmnd  18685  xpsgrp  18972  efgval  19630  efgtf  19635  frgpcpbl  19672  frgp0  19673  frgpeccl  19674  frgpadd  19676  frgpmhm  19678  vrgpf  19681  vrgpinv  19682  frgpupf  19686  frgpup1  19688  frgpup2  19689  frgpup3lem  19690  frgpnabllem1  19786  frgpnabllem2  19787  xpsrngd  20098  xpsringd  20251  xpstopnlem1  23725  xpstps  23726  xpstopnlem2  23727  xpsxmetlem  24295  xpsdsval  24297  nofv  27597  sltres  27602  noextendgt  27610  nolesgn2ores  27612  nosepnelem  27619  nosepdmlem  27623  nolt02o  27635  nogt01o  27636  nosupno  27643  nosupbnd1lem3  27650  nosupbnd1  27654  nosupbnd2lem1  27655  nosupbnd2  27656  ssoninhaus  36488  onint1  36489  1oequni2o  37408  finxpreclem4  37434  pw2f1ocnv  43076  frlmpwfi  43137  omnord1  43344  oege2  43346  oenord1  43355  oaomoencom  43356  oenassex  43357  oenass  43358  omabs2  43371  oaltom  43444  omltoe  43446  2no  43476  nlim3  43483  tr3dom  43567  enrelmap  44036  nelsubc3  49109