Theorem 2onn 8569

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  Oncon0 6315  Lim wlim 6316  ωcom 7808  2_oc2o 8390

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 5368

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 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-om 7809  df-1o 8396  df-2o 8397

This theorem is referenced by:  3onn  8571  nn2m  8581  nnneo  8582  nneob  8583  omopthlem1  8586  omopthlem2  8587  pwen  9079  prfi  9225  en2eqpr  9918  en2eleq  9919  unctb  10115  infdjuabs  10116  ackbij1lem5  10134  sdom2en01  10213  fin56  10304  fin67  10306  fin1a2lem4  10314  alephexp1  10491  pwcfsdom  10495  alephom  10497  canthp1lem2  10565  pwxpndom2  10577  hash3  14357  hash2pr  14420  pr2pwpr  14430  rpnnen  16183  rexpen  16184  xpsfrnel  17515  xpscf  17518  symggen  19434  psgnunilem1  19457  simpgnsgd  20066  znfld  21548  hauspwdom  23474  xpsmet  24355  xpsxms  24507  xpsms  24508  unidifsnel  32618  unidifsnne  32619  sat1el2xp  35575  ex-sategoelelomsuc  35622  ex-sategoelel12  35623  1oequni2o  37688  finxpreclem4  37714  finxp3o  37720  wepwso  43479  frlmpwfi  43534  2omomeqom  43739  oenord1ex  43751  oaomoencom  43753  2finon  43885  har2o  43981