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

Theorem 1onn 7099
Description: One is a natural number. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
1onn  |-  1o  e.  om

Proof of Theorem 1onn
StepHypRef Expression
1 df-1o 6941 . 2  |-  1o  =  suc  (/)
2 peano1 6516 . . 3  |-  (/)  e.  om
3 peano2 6517 . . 3  |-  ( (/)  e.  om  ->  suc  (/)  e.  om )
42, 3ax-mp 5 . 2  |-  suc  (/)  e.  om
51, 4eqeltri 2513 1  |-  1o  e.  om
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   (/)c0 3658   suc csuc 4742   omcom 6497   1oc1o 6934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552  ax-un 6393
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-tr 4407  df-eprel 4653  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-om 6498  df-1o 6941
This theorem is referenced by:  2onn  7100  oaabs2  7105  omabs  7107  nnm2  7109  nnneo  7111  nneob  7112  snfi  7411  1sdom2  7532  1sdom  7536  unxpdom2  7542  en1eqsn  7563  en2  7569  pwfi  7627  wofib  7780  oancom  7878  cnfcom3clem  7959  cnfcom3clemOLD  7967  card1  8159  pm54.43lem  8190  en2eleq  8196  en2other2  8197  infxpenlem  8201  infxpenc2lem1  8206  infmap2  8408  sdom2en01  8492  cfpwsdom  8769  canthp1lem2  8841  gchcda1  8844  pwxpndom2  8853  pwcdandom  8855  1pi  9073  1lt2pi  9095  indpi  9097  hash2  12184  hash1snb  12192  euhash1  12193  setcepi  14977  f1otrspeq  15974  pmtrf  15982  pmtrmvd  15983  pmtrfinv  15988  lt6abl  16392  isnzr2  17367  vr1cl  17693  ply1coe  17768  ply1coeOLD  17769  frgpcyg  18028  isppw  22474  snnen2o  30767  bnj906  32019
  Copyright terms: Public domain W3C validator