Theorem 2on 7852

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 ∈ On

Proof of Theorem 2on

Step	Hyp	Ref	Expression
1		df-2o 7844	. 2 ⊢ 2o = suc 1o
2		1on 7850	. . 3 ⊢ 1o ∈ On
3	2	onsuci 7316	. 2 ⊢ suc 1o ∈ On
4	1, 3	eqeltri 2854	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2106  Oncon0 5976  suc csuc 5978  1_oc1o 7836  2_oc2o 7837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pr 5138  ax-un 7226

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-sbc 3652  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-tr 4988  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-ord 5979  df-on 5980  df-suc 5982  df-1o 7843  df-2o 7844

This theorem is referenced by:  3on  7854  o2p2e4  7905  oneo  7945  nneob  8016  infxpenc  9174  infxpenc2  9178  mappwen  9268  pwcdaen  9342  ackbij1lem5  9381  sdom2en01  9459  fin1a2lem4  9560  fin1a2lem6  9562  xpslem  16619  xpsadd  16622  xpsmul  16623  xpsvsca  16625  xpsle  16627  xpsmnd  17716  xpsgrp  17921  efgval  18514  efgtf  18519  frgpcpbl  18558  frgp0  18559  frgpeccl  18560  frgpadd  18562  frgpmhm  18564  vrgpf  18567  vrgpinv  18568  frgpupf  18572  frgpup1  18574  frgpup2  18575  frgpup3lem  18576  frgpnabllem1  18662  frgpnabllem2  18663  xpstopnlem1  22021  xpstps  22022  xpstopnlem2  22023  xpsxmetlem  22592  xpsdsval  22594  nofv  32399  sltres  32404  noextendgt  32412  nolesgn2ores  32414  nosepnelem  32419  nosepdmlem  32422  nolt02o  32434  nosupno  32438  nosupbday  32440  nosupbnd1lem3  32445  nosupbnd1  32449  nosupbnd2lem1  32450  nosupbnd2  32451  ssoninhaus  33030  onint1  33031  1oequni2o  33811  finxpreclem4  33826  pw2f1ocnv  38545  frlmpwfi  38609  enrelmap  39229  clsk1indlem1  39281  clsk1independent  39282