Theorem 2on 8493

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8480	. 2 ⊢ 2o = suc 1o
2		1on 8492	. . 3 ⊢ 1o ∈ On
3		2oex 8491	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2857	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7823	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 705	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2856	1 ⊢ 2o ∈ On

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  Oncon0 6362  suc csuc 6364  1_oc1o 8472  2_oc2o 8473

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366  df-suc 6368  df-1o 8479  df-2o 8480

This theorem is used by:  ord3  8495  3on  8496  ord2eln012  8508  o2p2e4  8552  oneo  8592  2onn  8654  nneob  8668  en3  9275  infxpenc  10100  infxpenc2  10104  mappwen  10194  pwdjuen  10263  ackbij1lem5  10304  sdom2en01  10383  fin1a2lem4  10484  fin1a2lem6  10486  xpsrnbas  17748  xpsadd  17751  xpsmul  17752  xpsvsca  17754  xpsle  17756  cat1  18277  xpsmnd  18976  xpsgrp  19274  efgval  19936  efgtf  19941  frgpcpbl  19978  frgp0  19979  frgpeccl  19980  frgpadd  19982  frgpmhm  19984  vrgpf  19987  vrgpinv  19988  frgpupf  19992  frgpup1  19994  frgpup2  19995  frgpup3lem  19996  frgpnabllem1  20092  frgpnabllem2  20093  xpsrngd  20406  xpsringd  20567  xpstopnlem1  24133  xpstps  24134  xpstopnlem2  24135  xpsxmetlem  24703  xpsdsval  24705  nofv  28019  ltsres  28024  noextendgt  28032  nolesgn2ores  28034  nosepnelem  28041  nosepdmlem  28045  nolt02o  28057  nogt01o  28058  nosupno  28065  nosupbnd1lem3  28072  nosupbnd1  28076  nosupbnd2lem1  28077  nosupbnd2  28078  bdaypw2n0bndlem  28854  ssoninhaus  37328  onint1  37329  1oequni2o  38384  finxpreclem4  38410  pw2f1ocnv  44137  frlmpwfi  44193  omnord1  44400  oege2  44402  oenord1  44411  oaomoencom  44412  oenassex  44413  oenass  44414  omabs2  44427  oaltom  44499  omltoe  44501  2fno  44531  nlim3  44538  tr3dom  44622  enrelmap  45090  nelsubc3  50278  par2catid  50860  parswapprop  50870