Theorem 2onn 8570

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113  Oncon0 6317  Lim wlim 6318  ωcom 7808  2_oc2o 8391

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 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-tr 5206  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-om 7809  df-1o 8397  df-2o 8398

This theorem is referenced by:  3onn  8572  nn2m  8582  nnneo  8583  nneob  8584  omopthlem1  8587  omopthlem2  8588  pwen  9078  prfi  9224  en2eqpr  9917  en2eleq  9918  unctb  10114  infdjuabs  10115  ackbij1lem5  10133  sdom2en01  10212  fin56  10303  fin67  10305  fin1a2lem4  10313  alephexp1  10490  pwcfsdom  10494  alephom  10496  canthp1lem2  10564  pwxpndom2  10576  hash3  14329  hash2pr  14392  pr2pwpr  14402  rpnnen  16152  rexpen  16153  xpsfrnel  17483  xpscf  17486  symggen  19399  psgnunilem1  19422  simpgnsgd  20031  znfld  21515  hauspwdom  23445  xpsmet  24326  xpsxms  24478  xpsms  24479  unidifsnel  32610  unidifsnne  32611  sat1el2xp  35573  ex-sategoelelomsuc  35620  ex-sategoelel12  35621  1oequni2o  37569  finxpreclem4  37595  finxp3o  37601  wepwso  43281  frlmpwfi  43336  2omomeqom  43541  oenord1ex  43553  oaomoencom  43555  2finon  43687  har2o  43783