Theorem 2onn 8680

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2108  Oncon0 6384  Lim wlim 6385  ωcom 7887  2_oc2o 8500

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-om 7888  df-1o 8506  df-2o 8507

This theorem is referenced by:  3onn  8682  nn2m  8692  nnneo  8693  nneob  8694  omopthlem1  8697  omopthlem2  8698  pwen  9190  prfi  9363  en2eqpr  10047  en2eleq  10048  unctb  10244  infdjuabs  10245  ackbij1lem5  10263  sdom2en01  10342  fin56  10433  fin67  10435  fin1a2lem4  10443  alephexp1  10619  pwcfsdom  10623  alephom  10625  canthp1lem2  10693  pwxpndom2  10705  hash3  14445  hash2pr  14508  pr2pwpr  14518  rpnnen  16263  rexpen  16264  xpsfrnel  17607  xpscf  17610  symggen  19488  psgnunilem1  19511  simpgnsgd  20120  znfld  21579  hauspwdom  23509  xpsmet  24392  xpsxms  24547  xpsms  24548  unidifsnel  32553  unidifsnne  32554  sat1el2xp  35384  ex-sategoelelomsuc  35431  ex-sategoelel12  35432  1oequni2o  37369  finxpreclem4  37395  finxp3o  37401  wepwso  43055  frlmpwfi  43110  2omomeqom  43316  oenord1ex  43328  oaomoencom  43330  2finon  43463  har2o  43559