Theorem 2on 8113

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 8105	. 2 ⊢ 2o = suc 1o
2		1on 8111	. . 3 ⊢ 1o ∈ On
3	2	onsuci 7555	. 2 ⊢ suc 1o ∈ On
4	1, 3	eqeltri 2911	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2114  Oncon0 6193  suc csuc 6195  1_oc1o 8097  2_oc2o 8098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-tr 5175  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-ord 6196  df-on 6197  df-suc 6199  df-1o 8104  df-2o 8105

This theorem is referenced by:  3on  8116  o2p2e4  8168  o2p2e4OLD  8169  oneo  8209  nneob  8281  infxpenc  9446  infxpenc2  9450  mappwen  9540  pwdjuen  9609  ackbij1lem5  9648  sdom2en01  9726  fin1a2lem4  9827  fin1a2lem6  9829  xpsrnbas  16846  xpsadd  16849  xpsmul  16850  xpsvsca  16852  xpsle  16854  xpsmnd  17953  xpsgrp  18220  efgval  18845  efgtf  18850  frgpcpbl  18887  frgp0  18888  frgpeccl  18889  frgpadd  18891  frgpmhm  18893  vrgpf  18896  vrgpinv  18897  frgpupf  18901  frgpup1  18903  frgpup2  18904  frgpup3lem  18905  frgpnabllem1  18995  frgpnabllem2  18996  xpstopnlem1  22419  xpstps  22420  xpstopnlem2  22421  xpsxmetlem  22991  xpsdsval  22993  nofv  33166  sltres  33171  noextendgt  33179  nolesgn2ores  33181  nosepnelem  33186  nosepdmlem  33189  nolt02o  33201  nosupno  33205  nosupbday  33207  nosupbnd1lem3  33212  nosupbnd1  33216  nosupbnd2lem1  33217  nosupbnd2  33218  ssoninhaus  33798  onint1  33799  1oequni2o  34651  finxpreclem4  34677  pw2f1ocnv  39641  frlmpwfi  39705  tr3dom  39901  enrelmap  40350