Theorem 2onn 8563

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

Step	Hyp	Ref	Expression
1		2on 8404	. 2 ⊢ 2o ∈ On
2		2ellim 8420	. . 3 ⊢ (Lim 𝑥 → 2o ∈ 𝑥)
3	2	ax-gen 1796	. 2 ⊢ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)
4		elom 7805	. 2 ⊢ (2o ∈ ω ↔ (2o ∈ On ∧ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 711	1 ⊢ 2o ∈ ω

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113  Oncon0 6311  Lim wlim 6312  ωcom 7802  2_oc2o 8385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-tr 5201  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-om 7803  df-1o 8391  df-2o 8392

This theorem is referenced by:  3onn  8565  nn2m  8575  nnneo  8576  nneob  8577  omopthlem1  8580  omopthlem2  8581  pwen  9070  prfi  9215  en2eqpr  9905  en2eleq  9906  unctb  10102  infdjuabs  10103  ackbij1lem5  10121  sdom2en01  10200  fin56  10291  fin67  10293  fin1a2lem4  10301  alephexp1  10477  pwcfsdom  10481  alephom  10483  canthp1lem2  10551  pwxpndom2  10563  hash3  14315  hash2pr  14378  pr2pwpr  14388  rpnnen  16138  rexpen  16139  xpsfrnel  17468  xpscf  17471  symggen  19384  psgnunilem1  19407  simpgnsgd  20016  znfld  21499  hauspwdom  23417  xpsmet  24298  xpsxms  24450  xpsms  24451  unidifsnel  32517  unidifsnne  32518  sat1el2xp  35444  ex-sategoelelomsuc  35491  ex-sategoelel12  35492  1oequni2o  37433  finxpreclem4  37459  finxp3o  37465  wepwso  43161  frlmpwfi  43216  2omomeqom  43421  oenord1ex  43433  oaomoencom  43435  2finon  43568  har2o  43664