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

Theorem 2onn 7225
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 7067 . 2  |-  2o  =  suc  1o
2 1onn 7224 . . 3  |-  1o  e.  om
3 peano2 6637 . . 3  |-  ( 1o  e.  om  ->  suc  1o  e.  om )
42, 3ax-mp 5 . 2  |-  suc  1o  e.  om
51, 4eqeltri 2476 1  |-  2o  e.  om
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1836   suc csuc 4807   omcom 6617   1oc1o 7059   2oc2o 7060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pr 4614  ax-un 6509
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-tr 4474  df-eprel 4718  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-om 6618  df-1o 7066  df-2o 7067
This theorem is referenced by:  3onn  7226  nn2m  7235  nnneo  7236  nneob  7237  omopthlem1  7240  omopthlem2  7241  pwen  7627  en3  7690  en2eqpr  8316  en2eleq  8317  unctb  8516  infcdaabs  8517  ackbij1lem5  8535  sdom2en01  8613  fin56  8704  fin67  8706  fin1a2lem4  8714  alephexp1  8885  pwcfsdom  8889  alephom  8891  canthp1lem2  8960  pwxpndom2  8972  hash3  12394  hash2pr  12438  pr2pwpr  12443  rpnnen  13981  rexpen  13982  xpsfrnel  14989  symggen  16631  psgnunilem1  16654  znfld  18709  hauspwdom  20106  xpsmet  20989  xpsxms  21141  xpsms  21142  wepwso  31190  frlmpwfi  31250
  Copyright terms: Public domain W3C validator