Theorem 2onn 8667

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

Step	Hyp	Ref	Expression
1		2on 8505	. 2 ⊢ 2o ∈ On
2		2ellim 8524	. . 3 ⊢ (Lim 𝑥 → 2o ∈ 𝑥)
3	2	ax-gen 1789	. 2 ⊢ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)
4		elom 7877	. 2 ⊢ (2o ∈ ω ↔ (2o ∈ On ∧ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 709	1 ⊢ 2o ∈ ω

Syntax hints:   → wi 4  ∀wal 1531   ∈ wcel 2098  Oncon0 6372  Lim wlim 6373  ωcom 7874  2_oc2o 8485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698  ax-sep 5301  ax-nul 5308  ax-pr 5431

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-br 5151  df-opab 5213  df-tr 5268  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-we 5637  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-om 7875  df-1o 8491  df-2o 8492

This theorem is referenced by:  3onn  8669  nn2m  8679  nnneo  8680  nneob  8681  omopthlem1  8684  omopthlem2  8685  pwen  9179  en2eqpr  10036  en2eleq  10037  unctb  10234  infdjuabs  10235  ackbij1lem5  10253  sdom2en01  10331  fin56  10422  fin67  10424  fin1a2lem4  10432  alephexp1  10608  pwcfsdom  10612  alephom  10614  canthp1lem2  10682  pwxpndom2  10694  hash3  14403  hash2pr  14468  pr2pwpr  14478  rpnnen  16209  rexpen  16210  xpsfrnel  17549  xpscf  17552  symggen  19430  psgnunilem1  19453  simpgnsgd  20062  znfld  21499  hauspwdom  23423  xpsmet  24306  xpsxms  24461  xpsms  24462  unidifsnel  32349  unidifsnne  32350  sat1el2xp  34994  ex-sategoelelomsuc  35041  ex-sategoelel12  35042  1oequni2o  36852  finxpreclem4  36878  finxp3o  36884  wepwso  42470  frlmpwfi  42525  2omomeqom  42735  oenord1ex  42747  oaomoencom  42749  2finon  42883  har2o  42979