Theorem 2on 8311

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8298	. 2 ⊢ 2o = suc 1o
2		1on 8309	. . 3 ⊢ 1o ∈ On
3		2oex 8308	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2836	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7658	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 689	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2835	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2106  Vcvv 3432  Oncon0 6266  suc csuc 6268  1_oc1o 8290  2_oc2o 8291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-tr 5192  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-ord 6269  df-on 6270  df-suc 6272  df-1o 8297  df-2o 8298

This theorem is referenced by:  3on  8314  ord2eln012  8327  o2p2e4  8371  o2p2e4OLD  8372  oneo  8412  2onn  8472  nneob  8486  infxpenc  9774  infxpenc2  9778  mappwen  9868  pwdjuen  9937  ackbij1lem5  9980  sdom2en01  10058  fin1a2lem4  10159  fin1a2lem6  10161  xpsrnbas  17282  xpsadd  17285  xpsmul  17286  xpsvsca  17288  xpsle  17290  cat1  17812  xpsmnd  18425  xpsgrp  18694  efgval  19323  efgtf  19328  frgpcpbl  19365  frgp0  19366  frgpeccl  19367  frgpadd  19369  frgpmhm  19371  vrgpf  19374  vrgpinv  19375  frgpupf  19379  frgpup1  19381  frgpup2  19382  frgpup3lem  19383  frgpnabllem1  19474  frgpnabllem2  19475  xpstopnlem1  22960  xpstps  22961  xpstopnlem2  22962  xpsxmetlem  23532  xpsdsval  23534  nofv  33860  sltres  33865  noextendgt  33873  nolesgn2ores  33875  nosepnelem  33882  nosepdmlem  33886  nolt02o  33898  nogt01o  33899  nosupno  33906  nosupbnd1lem3  33913  nosupbnd1  33917  nosupbnd2lem1  33918  nosupbnd2  33919  ssoninhaus  34637  onint1  34638  1oequni2o  35539  finxpreclem4  35565  pw2f1ocnv  40859  frlmpwfi  40923  nlim3  41051  tr3dom  41135  enrelmap  41605