Theorem 2on 8473

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 8460	. 2 ⊢ 2o = suc 1o
2		1on 8472	. . 3 ⊢ 1o ∈ On
3		2oex 8471	. . . 4 ⊢ 2o ∈ V
4	1, 3	eqeltrri 2859	. . 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 2858	1 ⊢ 2o ∈ On

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453  Oncon0 6361  suc csuc 6363  1_oc1o 8452  2_oc2o 8453

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 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-tr 5217  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365  df-suc 6367  df-1o 8459  df-2o 8460

This theorem is used by:  ord3  8475  3on  8476  ord2eln012  8488  o2p2e4  8532  oneo  8572  2onn  8634  nneob  8648  en3  9255  infxpenc  10025  infxpenc2  10029  mappwen  10119  pwdjuen  10188  ackbij1lem5  10229  sdom2en01  10308  fin1a2lem4  10409  fin1a2lem6  10411  xpsrnbas  17663  xpsadd  17666  xpsmul  17667  xpsvsca  17669  xpsle  17671  cat1  18192  xpsmnd  18890  xpsgrp  19188  efgval  19850  efgtf  19855  frgpcpbl  19892  frgp0  19893  frgpeccl  19894  frgpadd  19896  frgpmhm  19898  vrgpf  19901  vrgpinv  19902  frgpupf  19906  frgpup1  19908  frgpup2  19909  frgpup3lem  19910  frgpnabllem1  20006  frgpnabllem2  20007  xpsrngd  20320  xpsringd  20479  xpstopnlem1  24041  xpstps  24042  xpstopnlem2  24043  xpsxmetlem  24611  xpsdsval  24613  nofv  27901  ltsres  27906  noextendgt  27914  nolesgn2ores  27916  nosepnelem  27923  nosepdmlem  27927  nolt02o  27939  nogt01o  27940  nosupno  27947  nosupbnd1lem3  27954  nosupbnd1  27958  nosupbnd2lem1  27959  nosupbnd2  27960  bdaypw2n0bndlem  28736  ssoninhaus  37075  onint1  37076  1oequni2o  38130  finxpreclem4  38156  pw2f1ocnv  43886  frlmpwfi  43947  omnord1  44154  oege2  44156  oenord1  44165  oaomoencom  44166  oenassex  44167  oenass  44168  omabs2  44181  oaltom  44253  omltoe  44255  2fno  44285  nlim3  44292  tr3dom  44376  enrelmap  44845  nelsubc3  50005