Theorem 2onn 6497

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 6393	. 2 ⊢ 2o = suc 1o
2		1onn 6496	. . 3 ⊢ 1o ∈ ω
3		peano2 4577	. . 3 ⊢ (1o ∈ ω → suc 1o ∈ ω)
4	2, 3	ax-mp 5	. 2 ⊢ suc 1o ∈ ω
5	1, 4	eqeltri 2243	1 ⊢ 2o ∈ ω

Syntax hints:   ∈ wcel 2141  suc csuc 4348  ωcom 4572  1_oc1o 6385  2_oc2o 6386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-nul 4113  ax-pow 4158  ax-pr 4192  ax-un 4416

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3566  df-sn 3587  df-pr 3588  df-uni 3795  df-int 3830  df-suc 4354  df-iom 4573  df-1o 6392  df-2o 6393

This theorem is referenced by:  3onn  6498  nn2m  6502  pw1fin  6884  nninfex  7094  infnninfOLD  7097  nnnninf  7098  isomnimap  7109  enomnilem  7110  fodjuf  7117  ismkvmap  7126  ismkvnex  7127  enmkvlem  7133  iswomnimap  7138  enwomnilem  7141  exmidonfinlem  7157  exmidfodomrlemr  7166  exmidfodomrlemrALT  7167  pw1ne3  7194  3nsssucpw1  7200  prarloclemarch2  7368  nq02m  7414  prarloclemlt  7442  prarloclemlo  7443  prarloclem3  7446  prarloclemn  7448  prarloclem5  7449  prarloclemcalc  7451  hash3  10735  unct  12384  2ssom  13759  2o01f  13951  pwle2  13953  pwf1oexmid  13954  subctctexmid  13956  0nninf  13959  nnsf  13960  nninfsellemdc  13965  nninfself  13968  nninffeq  13975  isomninnlem  13984  iswomninnlem  14003  ismkvnnlem  14006