Theorem 1onn 8687

Description: The ordinal 1 is a natural number. For a shorter proof using Peano's postulates that depends on ax-un 7783, see 1onnALT 8688. Lemma 2.2 of [Schloeder] p. 4. (Contributed by NM, 29-Oct-1995.) Avoid ax-un 7783. (Revised by BTernaryTau, 1-Dec-2024.)

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2147  Oncon0 6388  Lim wlim 6389  ωcom 7911  1_oc1o 8507

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 5255  ax-nul 5266  ax-pr 5398

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 4841  df-uni 4873  df-br 5109  df-opab 5174  df-tr 5219  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-om 7912  df-1o 8514

This theorem is used by:  2onnALT  8690  1one2o  8693  oaabs2  8696  omabs  8698  nnm2  8700  nnneo  8702  nneob  8703  snfi  9109  1sdom2ALT  9278  unxpdom2  9289  wofib  9576  oancom  9689  cnfcom3clem  9743  ssttrcl  9753  ttrcltr  9754  djurf1o  10031  card1  10086  pm54.43lem  10120  en2eleq  10126  en2other2  10127  infxpenlem  10131  infxpenc2lem1  10137  sdom2en01  10419  cfpwsdom  10708  canthp1lem2  10777  gchdju1  10780  pwxpndom2  10789  pwdjundom  10791  1pi  11007  1lt2pi  11029  indpi  11031  hash2  14590  hash1snb  14605  fnpr2o  17779  fvpr1o  17782  f1otrspeq  19712  pmtrf  19720  pmtrmvd  19721  pmtrfinv  19726  lt6abl  20160  isnzr2  20819  frgpcyg  21934  vr1cl  22590  ply1coe  22671  isppw  27498  bnj906  35671  fineqvnttrclse  35933  sat1el2xp  36352  satfv1fvfmla1  36396  satefvfmla1  36398  ex-sategoelelomsuc  36399  ex-sategoelel12  36400  finxpreclem1  38580  finxpreclem2  38581  finxp1o  38583  finxpreclem4  38585  finxp2o  38590  domalom  38595  onexoegt  44507  1oaomeqom  44556  oaabsb  44557  omnord1ex  44567  oaomoencom  44580  cantnftermord  44583  cantnf2  44588  omabs2  44595  omcl2  44596  1finon  44711  finona1cl  44715  1iscard  44804  hashnnsuc  46274