Theorem 2on 8518

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8505	. 2 ⊢ 2o = suc 1o
2		1on 8517	. . 3 ⊢ 1o ∈ On
3		2oex 8516	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2861	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7847	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 705	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2860	1 ⊢ 2o ∈ On

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  Oncon0 6380  suc csuc 6382  1_oc1o 8497  2_oc2o 8498

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-tr 5216  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6383  df-on 6384  df-suc 6386  df-1o 8504  df-2o 8505

This theorem is used by:  ord3  8520  3on  8521  ord2eln012  8533  o2p2e4  8577  oneo  8617  2onn  8679  nneob  8693  en3  9300  infxpenc  10124  infxpenc2  10128  mappwen  10218  pwdjuen  10287  ackbij1lem5  10328  sdom2en01  10407  fin1a2lem4  10508  fin1a2lem6  10510  xpsrnbas  17772  xpsadd  17775  xpsmul  17776  xpsvsca  17778  xpsle  17780  cat1  18301  xpsmnd  19000  xpsgrp  19298  efgval  19961  efgtf  19966  frgpcpbl  20003  frgp0  20004  frgpeccl  20005  frgpadd  20007  frgpmhm  20009  vrgpf  20012  vrgpinv  20013  frgpupf  20017  frgpup1  20019  frgpup2  20020  frgpup3lem  20021  frgpnabllem1  20117  frgpnabllem2  20118  xpsrngd  20431  xpsringd  20592  xpstopnlem1  24158  xpstps  24159  xpstopnlem2  24160  xpsxmetlem  24728  xpsdsval  24730  nofv  28044  ltsres  28049  noextendgt  28057  nolesgn2ores  28059  nosepnelem  28066  nosepdmlem  28070  nolt02o  28082  nogt01o  28083  nosupno  28090  nosupbnd1lem3  28097  nosupbnd1  28101  nosupbnd2lem1  28102  nosupbnd2  28103  bdaypw2n0bndlem  28879  2olt9o  35879  gdlopcfv2  35973  gdlopcfv3  35974  gdlopcfv4  35975  gdlopcfv5  35976  gdlopcfv6  35977  gdlopcfv7  35978  gdlopcfv8  35979  ssoninhaus  37414  onint1  37415  1oequni2o  38483  finxpreclem4  38509  pw2f1ocnv  44237  frlmpwfi  44293  omnord1  44499  oege2  44501  oenord1  44510  oaomoencom  44511  oenassex  44512  oenass  44513  omabs2  44526  oaltom  44598  omltoe  44600  2fno  44630  nlim3  44637  tr3dom  44721  enrelmap  45189  nelsubc3  50390  par2catid  50972  parswapprop  50982