Theorem 2onn 6524

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 6420	. 2 ⊢ 2o = suc 1o
2		1onn 6523	. . 3 ⊢ 1o ∈ ω
3		peano2 4596	. . 3 ⊢ (1o ∈ ω → suc 1o ∈ ω)
4	2, 3	ax-mp 5	. 2 ⊢ suc 1o ∈ ω
5	1, 4	eqeltri 2250	1 ⊢ 2o ∈ ω

Syntax hints:   ∈ wcel 2148  suc csuc 4367  ωcom 4591  1_oc1o 6412  2_oc2o 6413

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-uni 3812  df-int 3847  df-suc 4373  df-iom 4592  df-1o 6419  df-2o 6420

This theorem is referenced by:  3onn  6525  2ssom  6527  nn2m  6530  pw1fin  6912  nninfex  7122  infnninfOLD  7125  nnnninf  7126  isomnimap  7137  enomnilem  7138  fodjuf  7145  ismkvmap  7154  ismkvnex  7155  enmkvlem  7161  iswomnimap  7166  enwomnilem  7169  nninfdcinf  7171  nninfwlporlem  7173  nninfwlpoimlemg  7175  exmidonfinlem  7194  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  pw1ne3  7231  3nsssucpw1  7237  2onetap  7256  2omotaplemap  7258  2omotaplemst  7259  exmidmotap  7262  prarloclemarch2  7420  nq02m  7466  prarloclemlt  7494  prarloclemlo  7495  prarloclem3  7498  prarloclemn  7500  prarloclem5  7501  prarloclemcalc  7503  hash3  10795  unct  12445  xpsfrnel  12768  xpscf  12771  2o01f  14831  pwle2  14833  pwf1oexmid  14834  subctctexmid  14835  0nninf  14838  nnsf  14839  nninfsellemdc  14844  nninfself  14847  nninffeq  14854  isomninnlem  14863  iswomninnlem  14882  ismkvnnlem  14885