Theorem 2onn 8682

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

Assertion

Ref	Expression
2onn	⊢ 2o ∈ ω

Proof of Theorem 2onn

Step	Hyp	Ref	Expression
1		2on 8521	. 2 ⊢ 2o ∈ On
2		2ellim 8538	. . 3 ⊢ (Lim 𝑥 → 2o ∈ 𝑥)
3	2	ax-gen 1828	. 2 ⊢ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥)
4		elom 7907	. 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 2147  Oncon0 6383  Lim wlim 6384  ωcom 7904  2_oc2o 8501

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-tr 5217  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-om 7905  df-1o 8507  df-2o 8508

This theorem is used by:  3onn  8684  nn2m  8694  nnneo  8695  nneob  8696  omopthlem1  8699  omopthlem2  8700  pwen  9200  prfi  9346  en2eqpr  10116  en2eleq  10117  unctb  10312  infdjuabs  10313  ackbij1lem5  10331  sdom2en01  10410  fin56  10501  fin67  10503  fin1a2lem4  10511  alephexp1  10694  pwcfsdom  10698  alephom  10700  canthp1lem2  10768  pwxpndom2  10780  hash3  14580  hash2pr  14644  pr2pwpr  14654  rpnnen  16427  rexpen  16428  xpsfrnel  17766  xpscf  17769  symggen  19717  psgnunilem1  19740  simpgnsgd  20349  znfld  21899  hauspwdom  23853  xpsmet  24734  xpsxms  24886  xpsms  24887  unidifsnel  33206  unidifsnne  33207  sat1el2xp  36324  ex-sategoelelomsuc  36371  ex-sategoelel12  36372  1oequni2o  38496  finxpreclem4  38522  finxp3o  38528  wepwso  44254  frlmpwfi  44304  2omomeqom  44508  oenord1ex  44520  oaomoencom  44522  2finon  44654  har2o  44750