Theorem 2on 8447

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

Assertion

Ref	Expression
2on	⊢ 2o ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 8435	. 2 ⊢ 2o = suc 1o
2		1on 8446	. . 3 ⊢ 1o ∈ On
3		2oex 8445	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2825	. . 3 ⊢ suc 1o ∈ V
5		sucexeloni 7785	. . 3 ⊢ ((1o ∈ On ∧ suc 1o ∈ V) → suc 1o ∈ On)
6	2, 4, 5	mp2an 692	. 2 ⊢ suc 1o ∈ On
7	1, 6	eqeltri 2824	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2109  Vcvv 3447  Oncon0 6332  suc csuc 6334  1_oc1o 8427  2_oc2o 8428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336  df-suc 6338  df-1o 8434  df-2o 8435

This theorem is referenced by:  ord3  8449  3on  8450  ord2eln012  8461  o2p2e4  8505  oneo  8545  2onn  8606  nneob  8620  en3  9227  infxpenc  9971  infxpenc2  9975  mappwen  10065  pwdjuen  10135  ackbij1lem5  10176  sdom2en01  10255  fin1a2lem4  10356  fin1a2lem6  10358  xpsrnbas  17534  xpsadd  17537  xpsmul  17538  xpsvsca  17540  xpsle  17542  cat1  18059  xpsmnd  18704  xpsgrp  18991  efgval  19647  efgtf  19652  frgpcpbl  19689  frgp0  19690  frgpeccl  19691  frgpadd  19693  frgpmhm  19695  vrgpf  19698  vrgpinv  19699  frgpupf  19703  frgpup1  19705  frgpup2  19706  frgpup3lem  19707  frgpnabllem1  19803  frgpnabllem2  19804  xpsrngd  20088  xpsringd  20241  xpstopnlem1  23696  xpstps  23697  xpstopnlem2  23698  xpsxmetlem  24267  xpsdsval  24269  nofv  27569  sltres  27574  noextendgt  27582  nolesgn2ores  27584  nosepnelem  27591  nosepdmlem  27595  nolt02o  27607  nogt01o  27608  nosupno  27615  nosupbnd1lem3  27622  nosupbnd1  27626  nosupbnd2lem1  27627  nosupbnd2  27628  ssoninhaus  36436  onint1  36437  1oequni2o  37356  finxpreclem4  37382  pw2f1ocnv  43026  frlmpwfi  43087  omnord1  43294  oege2  43296  oenord1  43305  oaomoencom  43306  oenassex  43307  oenass  43308  omabs2  43321  oaltom  43394  omltoe  43396  2no  43426  nlim3  43433  tr3dom  43517  enrelmap  43986  nelsubc3  49060