Theorem 2onn 8635

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

Step	Hyp	Ref	Expression
1		2on 8474	. 2 ⊢ 2o ∈ On
2		2ellim 8491	. . 3 ⊢ (Lim 𝑥 → 2o ∈ 𝑥)
3	2	ax-gen 1828	. 2 ⊢ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)
4		elom 7869	. 2 ⊢ (2o ∈ ω ↔ (2o ∈ On ∧ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 724	1 ⊢ 2o ∈ ω

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2145  Oncon0 6355  Lim wlim 6356  ωcom 7866  2_oc2o 8454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-om 7867  df-1o 8460  df-2o 8461

This theorem is used by:  3onn  8637  nn2m  8647  nnneo  8648  nneob  8649  omopthlem1  8652  omopthlem2  8653  pwen  9153  prfi  9299  en2eqpr  10067  en2eleq  10068  unctb  10263  infdjuabs  10264  ackbij1lem5  10282  sdom2en01  10361  fin56  10452  fin67  10454  fin1a2lem4  10462  alephexp1  10645  pwcfsdom  10649  alephom  10651  canthp1lem2  10719  pwxpndom2  10731  hash3  14530  hash2pr  14594  pr2pwpr  14604  rpnnen  16375  rexpen  16376  xpsfrnel  17714  xpscf  17717  symggen  19664  psgnunilem1  19687  simpgnsgd  20296  znfld  21846  hauspwdom  23800  xpsmet  24681  xpsxms  24833  xpsms  24834  unidifsnel  33113  unidifsnne  33114  sat1el2xp  36113  ex-sategoelelomsuc  36160  ex-sategoelel12  36161  1oequni2o  38259  finxpreclem4  38285  finxp3o  38291  wepwso  44003  frlmpwfi  44058  2omomeqom  44263  oenord1ex  44275  oaomoencom  44277  2finon  44409  har2o  44505