Theorem 2on 8474

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8461	. 2 ⊢ 2o = suc 1o
2		1on 8473	. . 3 ⊢ 1o ∈ On
3		2oex 8472	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2858	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7812	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 705	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2857	1 ⊢ 2o ∈ On

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  Oncon0 6355  suc csuc 6357  1_oc1o 8453  2_oc2o 8454

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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6358  df-on 6359  df-suc 6361  df-1o 8460  df-2o 8461

This theorem is used by:  ord3  8476  3on  8477  ord2eln012  8489  o2p2e4  8533  oneo  8573  2onn  8635  nneob  8649  en3  9256  infxpenc  10078  infxpenc2  10082  mappwen  10172  pwdjuen  10241  ackbij1lem5  10282  sdom2en01  10361  fin1a2lem4  10462  fin1a2lem6  10464  xpsrnbas  17723  xpsadd  17726  xpsmul  17727  xpsvsca  17729  xpsle  17731  cat1  18252  xpsmnd  18951  xpsgrp  19249  efgval  19911  efgtf  19916  frgpcpbl  19953  frgp0  19954  frgpeccl  19955  frgpadd  19957  frgpmhm  19959  vrgpf  19962  vrgpinv  19963  frgpupf  19967  frgpup1  19969  frgpup2  19970  frgpup3lem  19971  frgpnabllem1  20067  frgpnabllem2  20068  xpsrngd  20381  xpsringd  20542  xpstopnlem1  24108  xpstps  24109  xpstopnlem2  24110  xpsxmetlem  24678  xpsdsval  24680  nofv  27996  ltsres  28001  noextendgt  28009  nolesgn2ores  28011  nosepnelem  28018  nosepdmlem  28022  nolt02o  28034  nogt01o  28035  nosupno  28042  nosupbnd1lem3  28049  nosupbnd1  28053  nosupbnd2lem1  28054  nosupbnd2  28055  bdaypw2n0bndlem  28831  ssoninhaus  37206  onint1  37207  1oequni2o  38259  finxpreclem4  38285  pw2f1ocnv  43997  frlmpwfi  44058  omnord1  44265  oege2  44267  oenord1  44276  oaomoencom  44277  oenassex  44278  oenass  44279  omabs2  44292  oaltom  44364  omltoe  44366  2fno  44396  nlim3  44403  tr3dom  44487  enrelmap  44956  nelsubc3  50123