Theorem 2onn 8281

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 8118	. 2 ⊢ 2o = suc 1o
2		1onn 8280	. . 3 ⊢ 1o ∈ ω
3		peano2 7606	. . 3 ⊢ (1o ∈ ω → suc 1o ∈ ω)
4	2, 3	ax-mp 5	. 2 ⊢ suc 1o ∈ ω
5	1, 4	eqeltri 2848	1 ⊢ 2o ∈ ω

Syntax hints:   ∈ wcel 2111  suc csuc 6175  ωcom 7584  1_oc1o 8110  2_oc2o 8111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301  ax-un 7464

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-tr 5142  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-we 5488  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-om 7585  df-1o 8117  df-2o 8118

This theorem is referenced by:  3onn  8282  nn2m  8292  nnneo  8293  nneob  8294  omopthlem1  8297  omopthlem2  8298  pwen  8717  en3  8796  en2eqpr  9472  en2eleq  9473  unctb  9670  infdjuabs  9671  ackbij1lem5  9689  sdom2en01  9767  fin56  9858  fin67  9860  fin1a2lem4  9868  alephexp1  10044  pwcfsdom  10048  alephom  10050  canthp1lem2  10118  pwxpndom2  10130  hash3  13822  hash2pr  13884  pr2pwpr  13894  rpnnen  15633  rexpen  15634  xpsfrnel  16898  xpscf  16901  symggen  18670  psgnunilem1  18693  simpgnsgd  19295  znfld  20333  hauspwdom  22206  xpsmet  23089  xpsxms  23241  xpsms  23242  unidifsnel  30410  unidifsnne  30411  sat1el2xp  32861  ex-sategoelelomsuc  32908  ex-sategoelel12  32909  1oequni2o  35091  finxpreclem4  35117  finxp3o  35123  wepwso  40388  frlmpwfi  40443