Theorem 2onn 8654

Description: The ordinal 2 is a natural number. For a shorter proof using Peano's postulates that depends on ax-un 7729, see 2onnALT 8655. (Contributed by NM, 28-Sep-2004.) Avoid ax-un 7729. (Revised by BTernaryTau, 1-Dec-2024.)

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

Step	Hyp	Ref	Expression
1		2on 8494	. 2 ⊢ 2o ∈ On
2		2ellim 8511	. . 3 ⊢ (Lim 𝑥 → 2o ∈ 𝑥)
3	2	ax-gen 1795	. 2 ⊢ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)
4		elom 7864	. 2 ⊢ (2o ∈ ω ↔ (2o ∈ On ∧ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 711	1 ⊢ 2o ∈ ω

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2108  Oncon0 6352  Lim wlim 6353  ωcom 7861  2_oc2o 8474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-tr 5230  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-om 7862  df-1o 8480  df-2o 8481

This theorem is referenced by:  3onn  8656  nn2m  8666  nnneo  8667  nneob  8668  omopthlem1  8671  omopthlem2  8672  pwen  9164  prfi  9335  en2eqpr  10021  en2eleq  10022  unctb  10218  infdjuabs  10219  ackbij1lem5  10237  sdom2en01  10316  fin56  10407  fin67  10409  fin1a2lem4  10417  alephexp1  10593  pwcfsdom  10597  alephom  10599  canthp1lem2  10667  pwxpndom2  10679  hash3  14424  hash2pr  14487  pr2pwpr  14497  rpnnen  16245  rexpen  16246  xpsfrnel  17576  xpscf  17579  symggen  19451  psgnunilem1  19474  simpgnsgd  20083  znfld  21521  hauspwdom  23439  xpsmet  24321  xpsxms  24473  xpsms  24474  unidifsnel  32516  unidifsnne  32517  sat1el2xp  35401  ex-sategoelelomsuc  35448  ex-sategoelel12  35449  1oequni2o  37386  finxpreclem4  37412  finxp3o  37418  wepwso  43067  frlmpwfi  43122  2omomeqom  43327  oenord1ex  43339  oaomoencom  43341  2finon  43474  har2o  43570