Theorem 2onn 8609

Description: The ordinal 2 is a natural number. For a shorter proof using Peano's postulates that depends on ax-un 7714, see 2onnALT 8610. (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 8450	. 2 ⊢ 2o ∈ On
2		2ellim 8466	. . 3 ⊢ (Lim 𝑥 → 2o ∈ 𝑥)
3	2	ax-gen 1795	. 2 ⊢ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)
4		elom 7848	. 2 ⊢ (2o ∈ ω ↔ (2o ∈ On ∧ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 711	1 ⊢ 2o ∈ ω

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  Oncon0 6335  Lim wlim 6336  ωcom 7845  2_oc2o 8431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-om 7846  df-1o 8437  df-2o 8438

This theorem is referenced by:  3onn  8611  nn2m  8621  nnneo  8622  nneob  8623  omopthlem1  8626  omopthlem2  8627  pwen  9120  prfi  9281  en2eqpr  9967  en2eleq  9968  unctb  10164  infdjuabs  10165  ackbij1lem5  10183  sdom2en01  10262  fin56  10353  fin67  10355  fin1a2lem4  10363  alephexp1  10539  pwcfsdom  10543  alephom  10545  canthp1lem2  10613  pwxpndom2  10625  hash3  14378  hash2pr  14441  pr2pwpr  14451  rpnnen  16202  rexpen  16203  xpsfrnel  17532  xpscf  17535  symggen  19407  psgnunilem1  19430  simpgnsgd  20039  znfld  21477  hauspwdom  23395  xpsmet  24277  xpsxms  24429  xpsms  24430  unidifsnel  32471  unidifsnne  32472  sat1el2xp  35373  ex-sategoelelomsuc  35420  ex-sategoelel12  35421  1oequni2o  37363  finxpreclem4  37389  finxp3o  37395  wepwso  43039  frlmpwfi  43094  2omomeqom  43299  oenord1ex  43311  oaomoencom  43313  2finon  43446  har2o  43542