Theorem 1onn 8604

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

Step	Hyp	Ref	Expression
1		1on 8444	. 2 ⊢ 1o ∈ On
2		1ellim 8461	. . 3 ⊢ (Lim 𝑥 → 1o ∈ 𝑥)
3	2	ax-gen 1814	. 2 ⊢ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)
4		elom 7844	. 2 ⊢ (1o ∈ ω ↔ (1o ∈ On ∧ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 721	1 ⊢ 1o ∈ ω

Syntax hints:   → wi 4  ∀wal 1557   ∈ wcel 2141  Oncon0 6341  Lim wlim 6342  ωcom 7841  1_oc1o 8424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-tr 5205  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-om 7842  df-1o 8431

This theorem is referenced by:  2onnALT  8607  1one2o  8610  oaabs2  8613  omabs  8615  nnm2  8617  nnneo  8619  nneob  8620  snfi  9018  1sdom2ALT  9187  unxpdom2  9198  wofib  9487  oancom  9600  cnfcom3clem  9654  ssttrcl  9664  ttrcltr  9665  djurf1o  9865  card1  9920  pm54.43lem  9952  en2eleq  9958  en2other2  9959  infxpenlem  9963  infxpenc2lem1  9969  sdom2en01  10253  cfpwsdom  10536  canthp1lem2  10605  gchdju1  10608  pwxpndom2  10617  pwdjundom  10619  1pi  10835  1lt2pi  10857  indpi  10859  hash2  14412  hash1snb  14426  fnpr2o  17578  fvpr1o  17581  f1otrspeq  19478  pmtrf  19486  pmtrmvd  19487  pmtrfinv  19492  lt6abl  19926  isnzr2  20555  frgpcyg  21613  vr1cl  22267  ply1coe  22349  isppw  27166  bnj906  35186  fineqvnttrclse  35381  sat1el2xp  35690  satfv1fvfmla1  35734  satefvfmla1  35736  ex-sategoelelomsuc  35737  ex-sategoelel12  35738  finxpreclem1  37844  finxpreclem2  37845  finxp1o  37847  finxpreclem4  37849  finxp2o  37854  domalom  37859  onexoegt  43782  1oaomeqom  43831  oaabsb  43832  omnord1ex  43842  oaomoencom  43855  cantnftermord  43858  cantnf2  43863  omabs2  43870  omcl2  43871  1finon  43986  finona1cl  43990  1iscard  44079