Theorem 1onn 8678

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2108  Oncon0 6384  Lim wlim 6385  ωcom 7887  1_oc1o 8499

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-om 7888  df-1o 8506

This theorem is referenced by:  2onnALT  8681  1one2o  8684  oaabs2  8687  omabs  8689  nnm2  8691  nnneo  8693  nneob  8694  snfi  9083  snfiOLD  9084  snnen2oOLD  9264  1sdom2ALT  9277  1sdomOLD  9285  unxpdom2  9290  en1eqsnOLD  9309  wofib  9585  oancom  9691  cnfcom3clem  9745  ssttrcl  9755  ttrcltr  9756  djurf1o  9953  card1  10008  pm54.43lem  10040  en2eleq  10048  en2other2  10049  infxpenlem  10053  infxpenc2lem1  10059  sdom2en01  10342  cfpwsdom  10624  canthp1lem2  10693  gchdju1  10696  pwxpndom2  10705  pwdjundom  10707  1pi  10923  1lt2pi  10945  indpi  10947  hash2  14444  hash1snb  14458  fnpr2o  17602  fvpr1o  17605  f1otrspeq  19465  pmtrf  19473  pmtrmvd  19474  pmtrfinv  19479  lt6abl  19913  isnzr2  20518  frgpcyg  21592  vr1cl  22219  ply1coe  22302  isppw  27157  pw2bday  28418  bnj906  34944  sat1el2xp  35384  satfv1fvfmla1  35428  satefvfmla1  35430  ex-sategoelelomsuc  35431  ex-sategoelel12  35432  finxpreclem1  37390  finxpreclem2  37391  finxp1o  37393  finxpreclem4  37395  finxp2o  37400  domalom  37405  onexoegt  43256  1oaomeqom  43306  oaabsb  43307  omnord1ex  43317  oaomoencom  43330  cantnftermord  43333  cantnf2  43338  omabs2  43345  omcl2  43346  1finon  43462  finona1cl  43466  1iscard  43555