Theorem 2on 6916

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 6909	. 2 |- 2o = suc 1o
2		1on 6915	. . 3 |- 1o e. On
3	2	onsuci 6438	. 2 |- suc 1o e. On
4	1, 3	eqeltri 2503	1 |- 2o e. On

Syntax hints:   e. wcel 1755   Oncon0 4706   suc csuc 4708   1oc1o 6901   2oc2o 6902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519  ax-un 6361

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-tr 4374  df-eprel 4619  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-suc 4712  df-1o 6908  df-2o 6909

This theorem is referenced by:  3on  6918  oneo  7008  infxpenc  8172  infxpenc2  8176  infxpencOLD  8177  infxpenc2OLD  8180  mappwen  8270  pwcdaen  8342  sdom2en01  8459  fin1a2lem4  8560  xpslem  14494  xpsadd  14497  xpsmul  14498  xpsvsca  14500  xpsle  14502  xpsmnd  15444  xpsgrp  15654  efgval  16194  efgtf  16199  frgpcpbl  16236  frgp0  16237  frgpeccl  16238  frgpadd  16240  frgpmhm  16242  vrgpf  16245  vrgpinv  16246  frgpupf  16250  frgpup1  16252  frgpup2  16253  frgpup3lem  16254  frgpnabllem1  16331  frgpnabllem2  16332  xpstopnlem1  19224  xpstps  19225  xpstopnlem2  19226  xpsxmetlem  19796  xpsdsval  19798  nofv  27645  sltres  27652  noxp2o  27655  nobndup  27688  ssoninhaus  28142  onint1  28143  pw2f1ocnv  29231  frlmpwfi  29298