Theorem 2onn 6588

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 6484	. 2 ⊢ 2o = suc 1o
2		1onn 6587	. . 3 ⊢ 1o ∈ ω
3		peano2 4632	. . 3 ⊢ (1o ∈ ω → suc 1o ∈ ω)
4	2, 3	ax-mp 5	. 2 ⊢ suc 1o ∈ ω
5	1, 4	eqeltri 2269	1 ⊢ 2o ∈ ω

Syntax hints:   ∈ wcel 2167  suc csuc 4401  ωcom 4627  1_oc1o 6476  2_oc2o 6477

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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-nul 4160  ax-pow 4208  ax-pr 4243  ax-un 4469

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3452  df-pw 3608  df-sn 3629  df-pr 3630  df-uni 3841  df-int 3876  df-suc 4407  df-iom 4628  df-1o 6483  df-2o 6484

This theorem is referenced by:  3onn  6589  2ssom  6591  nn2m  6594  pw1fin  6980  nninfex  7196  infnninfOLD  7200  nnnninf  7201  isomnimap  7212  enomnilem  7213  fodjuf  7220  ismkvmap  7229  ismkvnex  7230  enmkvlem  7236  iswomnimap  7241  enwomnilem  7244  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemg  7250  exmidonfinlem  7272  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  pw1ne3  7313  3nsssucpw1  7319  2onetap  7338  2omotaplemap  7340  2omotaplemst  7341  exmidmotap  7344  prarloclemarch2  7503  nq02m  7549  prarloclemlt  7577  prarloclemlo  7578  prarloclem3  7581  prarloclemn  7583  prarloclem5  7584  prarloclemcalc  7586  hash3  10922  unct  12684  xpsfrnel  13046  xpscf  13049  znidom  14289  znidomb  14290  2o01f  15725  2omap  15726  2omapen  15727  pwle2  15729  pwf1oexmid  15730  subctctexmid  15731  0nninf  15735  nnsf  15736  nninfsellemdc  15741  nninfself  15744  nninffeq  15751  isomninnlem  15761  iswomninnlem  15780  ismkvnnlem  15783