Theorem 1onn 8676

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

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

Syntax hints:   → wi 4  ∀wal 1534   ∈ wcel 2105  Oncon0 6385  Lim wlim 6386  ωcom 7886  1_oc1o 8497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-om 7887  df-1o 8504

This theorem is referenced by:  2onnALT  8679  1one2o  8682  oaabs2  8685  omabs  8687  nnm2  8689  nnneo  8691  nneob  8692  snfi  9081  snfiOLD  9082  snnen2oOLD  9261  1sdom2ALT  9274  1sdomOLD  9282  unxpdom2  9287  en1eqsnOLD  9306  wofib  9582  oancom  9688  cnfcom3clem  9742  ssttrcl  9752  ttrcltr  9753  djurf1o  9950  card1  10005  pm54.43lem  10037  en2eleq  10045  en2other2  10046  infxpenlem  10050  infxpenc2lem1  10056  sdom2en01  10339  cfpwsdom  10621  canthp1lem2  10690  gchdju1  10693  pwxpndom2  10702  pwdjundom  10704  1pi  10920  1lt2pi  10942  indpi  10944  hash2  14440  hash1snb  14454  fnpr2o  17603  fvpr1o  17606  f1otrspeq  19479  pmtrf  19487  pmtrmvd  19488  pmtrfinv  19493  lt6abl  19927  isnzr2  20534  frgpcyg  21609  vr1cl  22234  ply1coe  22317  isppw  27171  pw2bday  28432  bnj906  34922  sat1el2xp  35363  satfv1fvfmla1  35407  satefvfmla1  35409  ex-sategoelelomsuc  35410  ex-sategoelel12  35411  finxpreclem1  37371  finxpreclem2  37372  finxp1o  37374  finxpreclem4  37376  finxp2o  37381  domalom  37386  onexoegt  43232  1oaomeqom  43282  oaabsb  43283  omnord1ex  43293  oaomoencom  43306  cantnftermord  43309  cantnf2  43314  omabs2  43321  omcl2  43322  1finon  43438  finona1cl  43442  1iscard  43531