Theorem 2on 7568

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 7561	. 2 |- 2o = suc 1o
2		1on 7567	. . 3 |- 1o e. On
3	2	onsuci 7038	. 2 |- suc 1o e. On
4	1, 3	eqeltri 2697	1 |- 2o e. On

Syntax hints:   e. wcel 1990   Oncon0 5723   suc csuc 5725   1oc1o 7553   2oc2o 7554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-tr 4753  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-ord 5726  df-on 5727  df-suc 5729  df-1o 7560  df-2o 7561

This theorem is referenced by:  3on  7570  o2p2e4  7621  oneo  7661  infxpenc  8841  infxpenc2  8845  mappwen  8935  pwcdaen  9007  sdom2en01  9124  fin1a2lem4  9225  xpslem  16233  xpsadd  16236  xpsmul  16237  xpsvsca  16239  xpsle  16241  xpsmnd  17330  xpsgrp  17534  efgval  18130  efgtf  18135  frgpcpbl  18172  frgp0  18173  frgpeccl  18174  frgpadd  18176  frgpmhm  18178  vrgpf  18181  vrgpinv  18182  frgpupf  18186  frgpup1  18188  frgpup2  18189  frgpup3lem  18190  frgpnabllem1  18276  frgpnabllem2  18277  xpstopnlem1  21612  xpstps  21613  xpstopnlem2  21614  xpsxmetlem  22184  xpsdsval  22186  nofv  31810  sltres  31815  noextendgt  31823  nolesgn2ores  31825  nosepnelem  31830  nosepdmlem  31833  nolt02o  31845  nosupno  31849  nosupbday  31851  nosupbnd1lem3  31856  nosupbnd1  31860  nosupbnd2lem1  31861  nosupbnd2  31862  ssoninhaus  32447  onint1  32448  1oequni2o  33216  finxpreclem4  33231  pw2f1ocnv  37604  frlmpwfi  37668  enrelmap  38291  clsk1indlem1  38343  clsk1independent  38344