Theorem 2onn 8607

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

Step	Hyp	Ref	Expression
1		2on 8446	. 2 ⊢ 2o ∈ On
2		2ellim 8463	. . 3 ⊢ (Lim 𝑥 → 2o ∈ 𝑥)
3	2	ax-gen 1814	. 2 ⊢ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)
4		elom 7845	. 2 ⊢ (2o ∈ ω ↔ (2o ∈ On ∧ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 721	1 ⊢ 2o ∈ ω

Syntax hints:   → wi 4  ∀wal 1557   ∈ wcel 2141  Oncon0 6342  Lim wlim 6343  ωcom 7842  2_oc2o 8426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-tr 5207  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-om 7843  df-1o 8432  df-2o 8433

This theorem is referenced by:  3onn  8609  nn2m  8619  nnneo  8620  nneob  8621  omopthlem1  8624  omopthlem2  8625  pwen  9118  prfi  9264  en2eqpr  9960  en2eleq  9961  unctb  10157  infdjuabs  10158  ackbij1lem5  10176  sdom2en01  10256  fin56  10347  fin67  10349  fin1a2lem4  10357  alephexp1  10534  pwcfsdom  10538  alephom  10540  canthp1lem2  10608  pwxpndom2  10620  hash3  14416  hash2pr  14479  pr2pwpr  14489  rpnnen  16242  rexpen  16243  xpsfrnel  17575  xpscf  17578  symggen  19493  psgnunilem1  19516  simpgnsgd  20125  znfld  21592  hauspwdom  23541  xpsmet  24422  xpsxms  24574  xpsms  24575  unidifsnel  32683  unidifsnne  32684  sat1el2xp  35693  ex-sategoelelomsuc  35740  ex-sategoelel12  35741  1oequni2o  37826  finxpreclem4  37852  finxp3o  37858  wepwso  43584  frlmpwfi  43639  2omomeqom  43844  oenord1ex  43856  oaomoencom  43858  2finon  43990  har2o  44086