Theorem 2on 7739

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	⊢ 2𝑜 ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 7731	. 2 ⊢ 2𝑜 = suc 1𝑜
2		1on 7737	. . 3 ⊢ 1𝑜 ∈ On
3	2	onsuci 7204	. 2 ⊢ suc 1𝑜 ∈ On
4	1, 3	eqeltri 2835	1 ⊢ 2𝑜 ∈ On

Syntax hints:   ∈ wcel 2139  Oncon0 5884  suc csuc 5886  1_𝑜c1o 7723  2_𝑜c2o 7724

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055  ax-un 7115

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-tr 4905  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-ord 5887  df-on 5888  df-suc 5890  df-1o 7730  df-2o 7731

This theorem is referenced by:  3on  7741  o2p2e4  7792  oneo  7832  infxpenc  9051  infxpenc2  9055  mappwen  9145  pwcdaen  9219  sdom2en01  9336  fin1a2lem4  9437  xpslem  16455  xpsadd  16458  xpsmul  16459  xpsvsca  16461  xpsle  16463  xpsmnd  17551  xpsgrp  17755  efgval  18350  efgtf  18355  frgpcpbl  18392  frgp0  18393  frgpeccl  18394  frgpadd  18396  frgpmhm  18398  vrgpf  18401  vrgpinv  18402  frgpupf  18406  frgpup1  18408  frgpup2  18409  frgpup3lem  18410  frgpnabllem1  18496  frgpnabllem2  18497  xpstopnlem1  21834  xpstps  21835  xpstopnlem2  21836  xpsxmetlem  22405  xpsdsval  22407  nofv  32137  sltres  32142  noextendgt  32150  nolesgn2ores  32152  nosepnelem  32157  nosepdmlem  32160  nolt02o  32172  nosupno  32176  nosupbday  32178  nosupbnd1lem3  32183  nosupbnd1  32187  nosupbnd2lem1  32188  nosupbnd2  32189  ssoninhaus  32774  onint1  32775  1oequni2o  33545  finxpreclem4  33560  pw2f1ocnv  38124  frlmpwfi  38188  enrelmap  38811  clsk1indlem1  38863  clsk1independent  38864