Theorem 2onn 8578

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  Oncon0 6323  Lim wlim 6324  ωcom 7817  2_oc2o 8399

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-tr 5193  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-om 7818  df-1o 8405  df-2o 8406

This theorem is referenced by:  3onn  8580  nn2m  8590  nnneo  8591  nneob  8592  omopthlem1  8595  omopthlem2  8596  pwen  9088  prfi  9234  en2eqpr  9929  en2eleq  9930  unctb  10126  infdjuabs  10127  ackbij1lem5  10145  sdom2en01  10224  fin56  10315  fin67  10317  fin1a2lem4  10325  alephexp1  10502  pwcfsdom  10506  alephom  10508  canthp1lem2  10576  pwxpndom2  10588  hash3  14368  hash2pr  14431  pr2pwpr  14441  rpnnen  16194  rexpen  16195  xpsfrnel  17526  xpscf  17529  symggen  19445  psgnunilem1  19468  simpgnsgd  20077  znfld  21540  hauspwdom  23466  xpsmet  24347  xpsxms  24499  xpsms  24500  unidifsnel  32605  unidifsnne  32606  sat1el2xp  35561  ex-sategoelelomsuc  35608  ex-sategoelel12  35609  1oequni2o  37684  finxpreclem4  37710  finxp3o  37716  wepwso  43471  frlmpwfi  43526  2omomeqom  43731  oenord1ex  43743  oaomoencom  43745  2finon  43877  har2o  43973