Theorem 2onn 8654

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   ∈ wcel 2144  Oncon0 6362  Lim wlim 6363  ωcom 7877  2_oc2o 8473

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-om 7878  df-1o 8479  df-2o 8480

This theorem is used by:  3onn  8656  nn2m  8666  nnneo  8667  nneob  8668  omopthlem1  8671  omopthlem2  8672  pwen  9172  prfi  9318  en2eqpr  10089  en2eleq  10090  unctb  10285  infdjuabs  10286  ackbij1lem5  10304  sdom2en01  10383  fin56  10474  fin67  10476  fin1a2lem4  10484  alephexp1  10667  pwcfsdom  10671  alephom  10673  canthp1lem2  10741  pwxpndom2  10753  hash3  14553  hash2pr  14617  pr2pwpr  14627  rpnnen  16400  rexpen  16401  xpsfrnel  17739  xpscf  17742  symggen  19689  psgnunilem1  19712  simpgnsgd  20321  znfld  21871  hauspwdom  23825  xpsmet  24706  xpsxms  24858  xpsms  24859  unidifsnel  33178  unidifsnne  33179  sat1el2xp  36230  ex-sategoelelomsuc  36277  ex-sategoelel12  36278  1oequni2o  38384  finxpreclem4  38410  finxp3o  38416  wepwso  44143  frlmpwfi  44193  2omomeqom  44398  oenord1ex  44410  oaomoencom  44412  2finon  44544  har2o  44640