Theorem 2on 6920

Description: Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)

Assertion

Ref	Expression
2on	|- 2o e. On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 6913	. 2 |- 2o = suc 1o
2		1on 6919	. . 3 |- 1o e. On
3	2	onsuci 6444	. 2 |- suc 1o e. On
4	1, 3	eqeltri 2508	1 |- 2o e. On

Syntax hints:   e. wcel 1756   Oncon0 4714   suc csuc 4716   1oc1o 6905   2oc2o 6906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526  ax-un 6367

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-tr 4381  df-eprel 4627  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-suc 4720  df-1o 6912  df-2o 6913

This theorem is referenced by:  3on  6922  oneo  7012  infxpenc  8176  infxpenc2  8180  infxpencOLD  8181  infxpenc2OLD  8184  mappwen  8274  pwcdaen  8346  sdom2en01  8463  fin1a2lem4  8564  xpslem  14503  xpsadd  14506  xpsmul  14507  xpsvsca  14509  xpsle  14511  xpsmnd  15453  xpsgrp  15665  efgval  16205  efgtf  16210  frgpcpbl  16247  frgp0  16248  frgpeccl  16249  frgpadd  16251  frgpmhm  16253  vrgpf  16256  vrgpinv  16257  frgpupf  16261  frgpup1  16263  frgpup2  16264  frgpup3lem  16265  frgpnabllem1  16342  frgpnabllem2  16343  xpstopnlem1  19362  xpstps  19363  xpstopnlem2  19364  xpsxmetlem  19934  xpsdsval  19936  nofv  27767  sltres  27774  noxp2o  27777  nobndup  27810  ssoninhaus  28264  onint1  28265  pw2f1ocnv  29357  frlmpwfi  29424