Theorem 2onn 8634

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

Step	Hyp	Ref	Expression
1		2on 8473	. 2 ⊢ 2o ∈ On
2		2ellim 8490	. . 3 ⊢ (Lim 𝑥 → 2o ∈ 𝑥)
3	2	ax-gen 1828	. 2 ⊢ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)
4		elom 7869	. 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 2145  Oncon0 6361  Lim wlim 6362  ωcom 7866  2_oc2o 8453

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 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-tr 5217  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-om 7867  df-1o 8459  df-2o 8460

This theorem is used by:  3onn  8636  nn2m  8646  nnneo  8647  nneob  8648  omopthlem1  8651  omopthlem2  8652  pwen  9152  prfi  9297  en2eqpr  10014  en2eleq  10015  unctb  10210  infdjuabs  10211  ackbij1lem5  10229  sdom2en01  10308  fin56  10399  fin67  10401  fin1a2lem4  10409  alephexp1  10592  pwcfsdom  10596  alephom  10598  canthp1lem2  10666  pwxpndom2  10678  hash3  14474  hash2pr  14538  pr2pwpr  14548  rpnnen  16321  rexpen  16322  xpsfrnel  17654  xpscf  17657  symggen  19603  psgnunilem1  19626  simpgnsgd  20235  znfld  21779  hauspwdom  23733  xpsmet  24614  xpsxms  24766  xpsms  24767  unidifsnel  33018  unidifsnne  33019  sat1el2xp  35966  ex-sategoelelomsuc  36013  ex-sategoelel12  36014  1oequni2o  38130  finxpreclem4  38156  finxp3o  38162  wepwso  43892  frlmpwfi  43947  2omomeqom  44152  oenord1ex  44164  oaomoencom  44166  2finon  44298  har2o  44394