Theorem 2on 8476

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8463	. 2 ⊢ 2o = suc 1o
2		1on 8475	. . 3 ⊢ 1o ∈ On
3		2oex 8474	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2863	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7817	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 705	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2862	1 ⊢ 2o ∈ On

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458  Oncon0 6367  suc csuc 6369  1_oc1o 8455  2_oc2o 8456

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-tr 5224  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-ord 6370  df-on 6371  df-suc 6373  df-1o 8462  df-2o 8463

This theorem is used by:  ord3  8478  3on  8479  ord2eln012  8491  o2p2e4  8535  oneo  8575  2onn  8637  nneob  8651  en3  9251  infxpenc  10021  infxpenc2  10025  mappwen  10115  pwdjuen  10184  ackbij1lem5  10225  sdom2en01  10304  fin1a2lem4  10405  fin1a2lem6  10407  xpsrnbas  17650  xpsadd  17653  xpsmul  17654  xpsvsca  17656  xpsle  17658  cat1  18179  xpsmnd  18866  xpsgrp  19156  efgval  19818  efgtf  19823  frgpcpbl  19860  frgp0  19861  frgpeccl  19862  frgpadd  19864  frgpmhm  19866  vrgpf  19869  vrgpinv  19870  frgpupf  19874  frgpup1  19876  frgpup2  19877  frgpup3lem  19878  frgpnabllem1  19974  frgpnabllem2  19975  xpsrngd  20288  xpsringd  20447  xpstopnlem1  24003  xpstps  24004  xpstopnlem2  24005  xpsxmetlem  24573  xpsdsval  24575  nofv  27858  ltsres  27863  noextendgt  27871  nolesgn2ores  27873  nosepnelem  27880  nosepdmlem  27884  nolt02o  27896  nogt01o  27897  nosupno  27904  nosupbnd1lem3  27911  nosupbnd1  27915  nosupbnd2lem1  27916  nosupbnd2  27917  bdaypw2n0bndlem  28693  ssoninhaus  37000  onint1  37001  1oequni2o  38055  finxpreclem4  38081  pw2f1ocnv  43805  frlmpwfi  43866  omnord1  44073  oege2  44075  oenord1  44084  oaomoencom  44085  oenassex  44086  oenass  44087  omabs2  44100  oaltom  44172  omltoe  44174  2fno  44204  nlim3  44211  tr3dom  44295  enrelmap  44764  nelsubc3  49890