MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2onn Structured version   Unicode version

Theorem 2onn 7352
Description: The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
Assertion
Ref Expression
2onn  |-  2o  e.  om

Proof of Theorem 2onn
StepHypRef Expression
1 df-2o 7194 . 2  |-  2o  =  suc  1o
2 1onn 7351 . . 3  |-  1o  e.  om
3 peano2 6727 . . 3  |-  ( 1o  e.  om  ->  suc  1o  e.  om )
42, 3ax-mp 5 . 2  |-  suc  1o  e.  om
51, 4eqeltri 2503 1  |-  2o  e.  om
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872   suc csuc 5444   omcom 6706   1oc1o 7186   2oc2o 7187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-tr 4519  df-eprel 4764  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-om 6707  df-1o 7193  df-2o 7194
This theorem is referenced by:  3onn  7353  nn2m  7362  nnneo  7363  nneob  7364  omopthlem1  7367  omopthlem2  7368  pwen  7754  en3  7817  en2eqpr  8446  en2eleq  8447  unctb  8642  infcdaabs  8643  ackbij1lem5  8661  sdom2en01  8739  fin56  8830  fin67  8832  fin1a2lem4  8840  alephexp1  9011  pwcfsdom  9015  alephom  9017  canthp1lem2  9085  pwxpndom2  9097  hash3  12589  hash2pr  12634  pr2pwpr  12640  rpnnen  14278  rexpen  14279  xpsfrnel  15468  symggen  17110  psgnunilem1  17133  znfld  19129  hauspwdom  20514  xpsmet  21395  xpsxms  21547  xpsms  21548  1oequni2o  31735  finxpreclem4  31750  finxp3o  31756  wepwso  35871  frlmpwfi  35926
  Copyright terms: Public domain W3C validator