Theorem 1onn 6731

Description: One is a natural number. (Contributed by NM, 29-Oct-1995.)

Assertion

Ref	Expression
1onn	|- 1o e. om

Proof of Theorem 1onn

Step	Hyp	Ref	Expression
1		df-1o 6625	. 2 |- 1o = suc (/)
2		peano1 4698	. . 3 |- (/) e. om
3		peano2 4699	. . 3 |- ( (/) e. om -> suc (/) e. om )
4	2, 3	ax-mp 5	. 2 |- suc (/) e. om
5	1, 4	eqeltri 2304	1 |- 1o e. om

Syntax hints:   e. wcel 2202   (/)c0 3496   suc csuc 4468   omcom 4694   1oc1o 6618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-nul 4220  ax-pow 4270  ax-pr 4305  ax-un 4536

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-nul 3497  df-pw 3658  df-sn 3679  df-pr 3680  df-uni 3899  df-int 3934  df-suc 4474  df-iom 4695  df-1o 6625

This theorem is referenced by:  2onn  6732  nnm2  6737  nnaordex  6739  snfig  7032  snnen2og  7088  1nen2  7090  1ndom2  7094  unfiexmid  7153  en1eqsn  7190  omp1eomlem  7353  fodjum  7405  fodju0  7406  nninfdcinf  7430  nninfwlporlemd  7431  nninfwlporlem  7432  en2eleq  7466  en2other2  7467  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  1pi  7595  1lt2pi  7620  archnqq  7697  nq0m0r  7736  nq02m  7745  prarloclemlt  7773  prarloclemlo  7774  1tonninf  10766  en1hash  11125  hash2  11139  fnpr2o  13502  fvpr1o  13505  upgrfi  16043  012of  16713  2omap  16715  pwle2  16720  peano3nninf  16733  nninfall  16735  nninfsellemdc  16736  nninfsellemeq  16740  nninfsellemeqinf  16742  nninffeq  16746  sbthom  16754  isomninnlem  16762  iswomninnlem  16782  ismkvnnlem  16785