Theorem 2onn 6754

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

Step	Hyp	Ref	Expression
1		df-2o 6648	. 2 |- 2o = suc 1o
2		1onn 6753	. . 3 |- 1o e. om
3		peano2 4717	. . 3 |- ( 1o e. om -> suc 1o e. om )
4	2, 3	ax-mp 5	. 2 |- suc 1o e. om
5	1, 4	eqeltri 2305	1 |- 2o e. om

Syntax hints:   e. wcel 2203   suc csuc 4486   omcom 4712   1oc1o 6640   2oc2o 6641

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 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-nul 4236  ax-pow 4287  ax-pr 4322  ax-un 4554

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-nul 3509  df-pw 3671  df-sn 3695  df-pr 3696  df-uni 3915  df-int 3950  df-suc 4492  df-iom 4713  df-1o 6647  df-2o 6648

This theorem is referenced by:  3onn  6755  2ssom  6757  nn2m  6760  1ndom2  7119  pw1fin  7170  2omap  7269  2omapen  7270  fipwfi  7272  nninfex  7412  infnninfOLD  7416  nnnninf  7417  isomnimap  7428  enomnilem  7429  fodjuf  7436  ismkvmap  7445  ismkvnex  7446  enmkvlem  7452  iswomnimap  7457  enwomnilem  7460  nninfdcinf  7462  nninfwlporlem  7464  nninfwlpoimlemg  7466  exmidonfinlem  7496  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  pw1ne3  7540  3nsssucpw1  7546  2onetap  7569  2omotaplemap  7571  2omotaplemst  7572  exmidmotap  7575  prarloclemarch2  7734  nq02m  7780  prarloclemlt  7808  prarloclemlo  7809  prarloclem3  7812  prarloclemn  7814  prarloclem5  7815  prarloclemcalc  7817  hash3  11178  hashpwfi  11193  hash2en  11215  unct  13193  xpsfrnel  13557  xpscf  13560  znidom  14805  znidomb  14806  upgrfi  16097  3dom  16762  2o01f  16768  pwle2  16772  pwf1oexmid  16773  subctctexmid  16774  0nninf  16782  nnsf  16783  nninfsellemdc  16788  nninfself  16791  nninffeq  16798  isomninnlem  16814  iswomninnlem  16834  ismkvnnlem  16837