Theorem 2on 8472

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8459	. 2 ⊢ 2o = suc 1o
2		1on 8471	. . 3 ⊢ 1o ∈ On
3		2oex 8470	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2859	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7811	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 705	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2858	1 ⊢ 2o ∈ On

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453  Oncon0 6361  suc csuc 6363  1_oc1o 8451  2_oc2o 8452

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-tr 5217  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365  df-suc 6367  df-1o 8458  df-2o 8459

This theorem is used by:  ord3  8474  3on  8475  ord2eln012  8487  o2p2e4  8531  oneo  8571  2onn  8633  nneob  8647  en3  9254  infxpenc  10024  infxpenc2  10028  mappwen  10118  pwdjuen  10187  ackbij1lem5  10228  sdom2en01  10307  fin1a2lem4  10408  fin1a2lem6  10410  xpsrnbas  17661  xpsadd  17664  xpsmul  17665  xpsvsca  17667  xpsle  17669  cat1  18190  xpsmnd  18888  xpsgrp  19186  efgval  19848  efgtf  19853  frgpcpbl  19890  frgp0  19891  frgpeccl  19892  frgpadd  19894  frgpmhm  19896  vrgpf  19899  vrgpinv  19900  frgpupf  19904  frgpup1  19906  frgpup2  19907  frgpup3lem  19908  frgpnabllem1  20004  frgpnabllem2  20005  xpsrngd  20318  xpsringd  20477  xpstopnlem1  24039  xpstps  24040  xpstopnlem2  24041  xpsxmetlem  24609  xpsdsval  24611  nofv  27894  ltsres  27899  noextendgt  27907  nolesgn2ores  27909  nosepnelem  27916  nosepdmlem  27920  nolt02o  27932  nogt01o  27933  nosupno  27940  nosupbnd1lem3  27947  nosupbnd1  27951  nosupbnd2lem1  27952  nosupbnd2  27953  bdaypw2n0bndlem  28729  ssoninhaus  37069  onint1  37070  1oequni2o  38124  finxpreclem4  38150  pw2f1ocnv  43880  frlmpwfi  43941  omnord1  44148  oege2  44150  oenord1  44159  oaomoencom  44160  oenassex  44161  oenass  44162  omabs2  44175  oaltom  44247  omltoe  44249  2fno  44279  nlim3  44286  tr3dom  44370  enrelmap  44839  nelsubc3  49999