Theorem 2onn 6753

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 6647	. 2 ⊢ 2o = suc 1o
2		1onn 6752	. . 3 ⊢ 1o ∈ ω
3		peano2 4716	. . 3 ⊢ (1o ∈ ω → suc 1o ∈ ω)
4	2, 3	ax-mp 5	. 2 ⊢ suc 1o ∈ ω
5	1, 4	eqeltri 2305	1 ⊢ 2o ∈ ω

Syntax hints:   ∈ wcel 2203  suc csuc 4485  ωcom 4711  1_oc1o 6639  2_oc2o 6640

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 4227  ax-nul 4235  ax-pow 4286  ax-pr 4321  ax-un 4553

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 2814  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-nul 3508  df-pw 3670  df-sn 3694  df-pr 3695  df-uni 3914  df-int 3949  df-suc 4491  df-iom 4712  df-1o 6646  df-2o 6647

This theorem is referenced by:  3onn  6754  2ssom  6756  nn2m  6759  1ndom2  7118  pw1fin  7169  2omap  7268  2omapen  7269  fipwfi  7271  nninfex  7411  infnninfOLD  7415  nnnninf  7416  isomnimap  7427  enomnilem  7428  fodjuf  7435  ismkvmap  7444  ismkvnex  7445  enmkvlem  7451  iswomnimap  7456  enwomnilem  7459  nninfdcinf  7461  nninfwlporlem  7463  nninfwlpoimlemg  7465  exmidonfinlem  7495  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  pw1ne3  7539  3nsssucpw1  7545  2onetap  7568  2omotaplemap  7570  2omotaplemst  7571  exmidmotap  7574  prarloclemarch2  7733  nq02m  7779  prarloclemlt  7807  prarloclemlo  7808  prarloclem3  7811  prarloclemn  7813  prarloclem5  7814  prarloclemcalc  7816  hash3  11176  hash2en  11211  unct  13185  xpsfrnel  13549  xpscf  13552  znidom  14797  znidomb  14798  upgrfi  16089  3dom  16754  2o01f  16760  pwle2  16764  pwf1oexmid  16765  subctctexmid  16766  0nninf  16774  nnsf  16775  nninfsellemdc  16780  nninfself  16783  nninffeq  16790  isomninnlem  16806  iswomninnlem  16826  ismkvnnlem  16829