Theorem 2onn 7666

Description: The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)

Assertion

Ref	Expression
2onn	⊢ 2𝑜 ∈ ω

Proof of Theorem 2onn

Step	Hyp	Ref	Expression
1		df-2o 7507	. 2 ⊢ 2𝑜 = suc 1𝑜
2		1onn 7665	. . 3 ⊢ 1𝑜 ∈ ω
3		peano2 7034	. . 3 ⊢ (1𝑜 ∈ ω → suc 1𝑜 ∈ ω)
4	2, 3	ax-mp 5	. 2 ⊢ suc 1𝑜 ∈ ω
5	1, 4	eqeltri 2700	1 ⊢ 2𝑜 ∈ ω

Syntax hints:   ∈ wcel 1992  suc csuc 5687  ωcom 7013  1_𝑜c1o 7499  2_𝑜c2o 7500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6903

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-tr 4718  df-eprel 4990  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-om 7014  df-1o 7506  df-2o 7507

This theorem is referenced by:  3onn  7667  nn2m  7676  nnneo  7677  nneob  7678  omopthlem1  7681  omopthlem2  7682  pwen  8078  en3  8142  en2eqpr  8775  en2eleq  8776  unctb  8972  infcdaabs  8973  ackbij1lem5  8991  sdom2en01  9069  fin56  9160  fin67  9162  fin1a2lem4  9170  alephexp1  9346  pwcfsdom  9350  alephom  9352  canthp1lem2  9420  pwxpndom2  9432  hash3  13131  hash2pr  13186  pr2pwpr  13194  rpnnen  14876  rexpen  14877  xpsfrnel  16139  symggen  17806  psgnunilem1  17829  znfld  19823  hauspwdom  21209  xpsmet  22092  xpsxms  22244  xpsms  22245  1oequni2o  32840  finxpreclem4  32855  finxp3o  32861  wepwso  37079  frlmpwfi  37134