Theorem 2onn 8575

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

Step	Hyp	Ref	Expression
1		2on 8415	. 2 ⊢ 2o ∈ On
2		2ellim 8431	. . 3 ⊢ (Lim 𝑥 → 2o ∈ 𝑥)
3	2	ax-gen 1802	. 2 ⊢ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)
4		elom 7816	. 2 ⊢ (2o ∈ ω ↔ (2o ∈ On ∧ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 717	1 ⊢ 2o ∈ ω

Syntax hints:   → wi 4  ∀wal 1545   ∈ wcel 2119  Oncon0 6317  Lim wlim 6318  ωcom 7813  2_oc2o 8396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-tr 5187  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-om 7814  df-1o 8402  df-2o 8403

This theorem is referenced by:  3onn  8577  nn2m  8587  nnneo  8588  nneob  8589  omopthlem1  8592  omopthlem2  8593  pwen  9085  prfi  9231  en2eqpr  9927  en2eleq  9928  unctb  10124  infdjuabs  10125  ackbij1lem5  10143  sdom2en01  10222  fin56  10313  fin67  10315  fin1a2lem4  10323  alephexp1  10500  pwcfsdom  10504  alephom  10506  canthp1lem2  10574  pwxpndom2  10586  hash3  14366  hash2pr  14429  pr2pwpr  14439  rpnnen  16192  rexpen  16193  xpsfrnel  17524  xpscf  17527  symggen  19443  psgnunilem1  19466  simpgnsgd  20075  znfld  21542  hauspwdom  23491  xpsmet  24372  xpsxms  24524  xpsms  24525  unidifsnel  32630  unidifsnne  32631  sat1el2xp  35614  ex-sategoelelomsuc  35661  ex-sategoelel12  35662  1oequni2o  37737  finxpreclem4  37763  finxp3o  37769  wepwso  43495  frlmpwfi  43550  2omomeqom  43755  oenord1ex  43767  oaomoencom  43769  2finon  43901  har2o  43997