Theorem 2on 8139

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 8132	. 2 ⊢ 2o = suc 1o
2		1on 8138	. . 3 ⊢ 1o ∈ On
3	2	onsuci 7572	. 2 ⊢ suc 1o ∈ On
4	1, 3	eqeltri 2829	1 ⊢ 2o ∈ On

Syntax hints:   ∈ wcel 2114  Oncon0 6172  suc csuc 6174  1_oc1o 8124  2_oc2o 8125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-11 2162  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296  ax-un 7479

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-br 5031  df-opab 5093  df-tr 5137  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-ord 6175  df-on 6176  df-suc 6178  df-1o 8131  df-2o 8132

This theorem is referenced by:  3on  8141  o2p2e4  8197  o2p2e4OLD  8198  oneo  8238  nneob  8310  infxpenc  9518  infxpenc2  9522  mappwen  9612  pwdjuen  9681  ackbij1lem5  9724  sdom2en01  9802  fin1a2lem4  9903  fin1a2lem6  9905  xpsrnbas  16947  xpsadd  16950  xpsmul  16951  xpsvsca  16953  xpsle  16955  cat1  17469  xpsmnd  18067  xpsgrp  18336  efgval  18961  efgtf  18966  frgpcpbl  19003  frgp0  19004  frgpeccl  19005  frgpadd  19007  frgpmhm  19009  vrgpf  19012  vrgpinv  19013  frgpupf  19017  frgpup1  19019  frgpup2  19020  frgpup3lem  19021  frgpnabllem1  19112  frgpnabllem2  19113  xpstopnlem1  22560  xpstps  22561  xpstopnlem2  22562  xpsxmetlem  23132  xpsdsval  23134  nofv  33501  sltres  33506  noextendgt  33514  nolesgn2ores  33516  nosepnelem  33523  nosepdmlem  33527  nolt02o  33539  nogt01o  33540  nosupno  33547  nosupbnd1lem3  33554  nosupbnd1  33558  nosupbnd2lem1  33559  nosupbnd2  33560  ssoninhaus  34275  onint1  34276  1oequni2o  35162  finxpreclem4  35188  pw2f1ocnv  40431  frlmpwfi  40495  tr3dom  40689  enrelmap  41151