Theorem 2onn 8637

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

Step	Hyp	Ref	Expression
1		2on 8476	. 2 ⊢ 2o ∈ On
2		2ellim 8493	. . 3 ⊢ (Lim 𝑥 → 2o ∈ 𝑥)
3	2	ax-gen 1828	. 2 ⊢ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)
4		elom 7874	. 2 ⊢ (2o ∈ ω ↔ (2o ∈ On ∧ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 724	1 ⊢ 2o ∈ ω

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2146  Oncon0 6367  Lim wlim 6368  ωcom 7871  2_oc2o 8456

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-tr 5224  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-om 7872  df-1o 8462  df-2o 8463

This theorem is used by:  3onn  8639  nn2m  8649  nnneo  8650  nneob  8651  omopthlem1  8654  omopthlem2  8655  pwen  9148  prfi  9293  en2eqpr  10010  en2eleq  10011  unctb  10206  infdjuabs  10207  ackbij1lem5  10225  sdom2en01  10304  fin56  10395  fin67  10397  fin1a2lem4  10405  alephexp1  10582  pwcfsdom  10586  alephom  10588  canthp1lem2  10656  pwxpndom2  10668  hash3  14462  hash2pr  14526  pr2pwpr  14536  rpnnen  16308  rexpen  16309  xpsfrnel  17641  xpscf  17644  symggen  19571  psgnunilem1  19594  simpgnsgd  20203  znfld  21747  hauspwdom  23695  xpsmet  24576  xpsxms  24728  xpsms  24729  unidifsnel  32918  unidifsnne  32919  sat1el2xp  35892  ex-sategoelelomsuc  35939  ex-sategoelel12  35940  1oequni2o  38055  finxpreclem4  38081  finxp3o  38087  wepwso  43811  frlmpwfi  43866  2omomeqom  44071  oenord1ex  44083  oaomoencom  44085  2finon  44217  har2o  44313