Theorem 2onn 8571

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

Step	Hyp	Ref	Expression
1		2on 8411	. 2 ⊢ 2o ∈ On
2		2ellim 8427	. . 3 ⊢ (Lim 𝑥 → 2o ∈ 𝑥)
3	2	ax-gen 1797	. 2 ⊢ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)
4		elom 7813	. 2 ⊢ (2o ∈ ω ↔ (2o ∈ On ∧ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 712	1 ⊢ 2o ∈ ω

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  Oncon0 6317  Lim wlim 6318  ωcom 7810  2_oc2o 8392

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-om 7811  df-1o 8398  df-2o 8399

This theorem is referenced by:  3onn  8573  nn2m  8583  nnneo  8584  nneob  8585  omopthlem1  8588  omopthlem2  8589  pwen  9081  prfi  9227  en2eqpr  9920  en2eleq  9921  unctb  10117  infdjuabs  10118  ackbij1lem5  10136  sdom2en01  10215  fin56  10306  fin67  10308  fin1a2lem4  10316  alephexp1  10493  pwcfsdom  10497  alephom  10499  canthp1lem2  10567  pwxpndom2  10579  hash3  14359  hash2pr  14422  pr2pwpr  14432  rpnnen  16185  rexpen  16186  xpsfrnel  17517  xpscf  17520  symggen  19436  psgnunilem1  19459  simpgnsgd  20068  znfld  21550  hauspwdom  23476  xpsmet  24357  xpsxms  24509  xpsms  24510  unidifsnel  32620  unidifsnne  32621  sat1el2xp  35577  ex-sategoelelomsuc  35624  ex-sategoelel12  35625  1oequni2o  37698  finxpreclem4  37724  finxp3o  37730  wepwso  43489  frlmpwfi  43544  2omomeqom  43749  oenord1ex  43761  oaomoencom  43763  2finon  43895  har2o  43991