Theorem 1onn 8604

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  Oncon0 6332  Lim wlim 6333  ωcom 7842  1_oc1o 8427

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

This theorem is referenced by:  2onnALT  8607  1one2o  8610  oaabs2  8613  omabs  8615  nnm2  8617  nnneo  8619  nneob  8620  snfi  9014  snfiOLD  9015  1sdom2ALT  9188  1sdomOLD  9196  unxpdom2  9201  en1eqsnOLD  9220  wofib  9498  oancom  9604  cnfcom3clem  9658  ssttrcl  9668  ttrcltr  9669  djurf1o  9866  card1  9921  pm54.43lem  9953  en2eleq  9961  en2other2  9962  infxpenlem  9966  infxpenc2lem1  9972  sdom2en01  10255  cfpwsdom  10537  canthp1lem2  10606  gchdju1  10609  pwxpndom2  10618  pwdjundom  10620  1pi  10836  1lt2pi  10858  indpi  10860  hash2  14370  hash1snb  14384  fnpr2o  17520  fvpr1o  17523  f1otrspeq  19377  pmtrf  19385  pmtrmvd  19386  pmtrfinv  19391  lt6abl  19825  isnzr2  20427  frgpcyg  21483  vr1cl  22102  ply1coe  22185  isppw  27024  bnj906  34920  sat1el2xp  35366  satfv1fvfmla1  35410  satefvfmla1  35412  ex-sategoelelomsuc  35413  ex-sategoelel12  35414  finxpreclem1  37377  finxpreclem2  37378  finxp1o  37380  finxpreclem4  37382  finxp2o  37387  domalom  37392  onexoegt  43233  1oaomeqom  43282  oaabsb  43283  omnord1ex  43293  oaomoencom  43306  cantnftermord  43309  cantnf2  43314  omabs2  43321  omcl2  43322  1finon  43438  finona1cl  43442  1iscard  43531