Theorem 2onn 8626

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2106  Oncon0 6354  Lim wlim 6355  ωcom 7839  2_oc2o 8444

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5293  ax-nul 5300  ax-pr 5421

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5143  df-opab 5205  df-tr 5260  df-eprel 5574  df-po 5582  df-so 5583  df-fr 5625  df-we 5627  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-om 7840  df-1o 8450  df-2o 8451

This theorem is referenced by:  3onn  8628  nn2m  8638  nnneo  8639  nneob  8640  omopthlem1  8643  omopthlem2  8644  pwen  9135  en2eqpr  9986  en2eleq  9987  unctb  10184  infdjuabs  10185  ackbij1lem5  10203  sdom2en01  10281  fin56  10372  fin67  10374  fin1a2lem4  10382  alephexp1  10558  pwcfsdom  10562  alephom  10564  canthp1lem2  10632  pwxpndom2  10644  hash3  14350  hash2pr  14414  pr2pwpr  14424  rpnnen  16154  rexpen  16155  xpsfrnel  17492  xpscf  17495  symggen  19304  psgnunilem1  19327  simpgnsgd  19931  znfld  21051  hauspwdom  22936  xpsmet  23819  xpsxms  23974  xpsms  23975  unidifsnel  31701  unidifsnne  31702  sat1el2xp  34265  ex-sategoelelomsuc  34312  ex-sategoelel12  34313  1oequni2o  36117  finxpreclem4  36143  finxp3o  36149  wepwso  41620  frlmpwfi  41675  2omomeqom  41888  oenord1ex  41900  oaomoencom  41902  2finon  42036  har2o  42132