Theorem 2onn 8606

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  Oncon0 6332  Lim wlim 6333  ωcom 7842  2_oc2o 8428

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-om 7843  df-1o 8434  df-2o 8435

This theorem is referenced by:  3onn  8608  nn2m  8618  nnneo  8619  nneob  8620  omopthlem1  8623  omopthlem2  8624  pwen  9114  prfi  9274  en2eqpr  9960  en2eleq  9961  unctb  10157  infdjuabs  10158  ackbij1lem5  10176  sdom2en01  10255  fin56  10346  fin67  10348  fin1a2lem4  10356  alephexp1  10532  pwcfsdom  10536  alephom  10538  canthp1lem2  10606  pwxpndom2  10618  hash3  14371  hash2pr  14434  pr2pwpr  14444  rpnnen  16195  rexpen  16196  xpsfrnel  17525  xpscf  17528  symggen  19400  psgnunilem1  19423  simpgnsgd  20032  znfld  21470  hauspwdom  23388  xpsmet  24270  xpsxms  24422  xpsms  24423  unidifsnel  32464  unidifsnne  32465  sat1el2xp  35366  ex-sategoelelomsuc  35413  ex-sategoelel12  35414  1oequni2o  37356  finxpreclem4  37382  finxp3o  37388  wepwso  43032  frlmpwfi  43087  2omomeqom  43292  oenord1ex  43304  oaomoencom  43306  2finon  43439  har2o  43535