Theorem 2onn 6657

Description: The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

Step	Hyp	Ref	Expression
1		df-2o 6553	. 2 ⊢ 2o = suc 1o
2		1onn 6656	. . 3 ⊢ 1o ∈ ω
3		peano2 4684	. . 3 ⊢ (1o ∈ ω → suc 1o ∈ ω)
4	2, 3	ax-mp 5	. 2 ⊢ suc 1o ∈ ω
5	1, 4	eqeltri 2302	1 ⊢ 2o ∈ ω

Syntax hints:   ∈ wcel 2200  suc csuc 4453  ωcom 4679  1_oc1o 6545  2_oc2o 6546

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-nul 4209  ax-pow 4257  ax-pr 4292  ax-un 4521

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-nul 3492  df-pw 3651  df-sn 3672  df-pr 3673  df-uni 3888  df-int 3923  df-suc 4459  df-iom 4680  df-1o 6552  df-2o 6553

This theorem is referenced by:  3onn  6658  2ssom  6660  nn2m  6663  1ndom2  7014  pw1fin  7060  nninfex  7276  infnninfOLD  7280  nnnninf  7281  isomnimap  7292  enomnilem  7293  fodjuf  7300  ismkvmap  7309  ismkvnex  7310  enmkvlem  7316  iswomnimap  7321  enwomnilem  7324  nninfdcinf  7326  nninfwlporlem  7328  nninfwlpoimlemg  7330  exmidonfinlem  7359  exmidfodomrlemr  7368  exmidfodomrlemrALT  7369  pw1ne3  7403  3nsssucpw1  7409  2onetap  7429  2omotaplemap  7431  2omotaplemst  7432  exmidmotap  7435  prarloclemarch2  7594  nq02m  7640  prarloclemlt  7668  prarloclemlo  7669  prarloclem3  7672  prarloclemn  7674  prarloclem5  7675  prarloclemcalc  7677  hash3  11022  hash2en  11052  unct  12999  xpsfrnel  13363  xpscf  13366  znidom  14606  znidomb  14607  upgrfi  15887  2o01f  16289  2omap  16290  2omapen  16291  pwle2  16295  pwf1oexmid  16296  subctctexmid  16297  0nninf  16301  nnsf  16302  nninfsellemdc  16307  nninfself  16310  nninffeq  16317  isomninnlem  16329  iswomninnlem  16348  ismkvnnlem  16351