Theorem 1onn 8622

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

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

Syntax hints:   → wi 4  ∀wal 1565   ∈ wcel 2149  Oncon0 6358  Lim wlim 6359  ωcom 7858  1_oc1o 8442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-tr 5220  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-om 7859  df-1o 8449

This theorem is referenced by:  2onnALT  8625  1one2o  8628  oaabs2  8631  omabs  8633  nnm2  8635  nnneo  8637  nneob  8638  snfi  9036  1sdom2ALT  9205  unxpdom2  9216  wofib  9503  oancom  9616  cnfcom3clem  9670  ssttrcl  9680  ttrcltr  9681  djurf1o  9895  card1  9950  pm54.43lem  9982  en2eleq  9988  en2other2  9989  infxpenlem  9993  infxpenc2lem1  9999  sdom2en01  10282  cfpwsdom  10565  canthp1lem2  10634  gchdju1  10637  pwxpndom2  10646  pwdjundom  10648  1pi  10864  1lt2pi  10886  indpi  10888  hash2  14437  hash1snb  14452  fnpr2o  17607  fvpr1o  17610  f1otrspeq  19513  pmtrf  19521  pmtrmvd  19522  pmtrfinv  19527  lt6abl  19961  isnzr2  20597  frgpcyg  21688  vr1cl  22342  ply1coe  22423  isppw  27240  bnj906  35259  fineqvnttrclse  35456  sat1el2xp  35766  satfv1fvfmla1  35810  satefvfmla1  35812  ex-sategoelelomsuc  35813  ex-sategoelel12  35814  finxpreclem1  37918  finxpreclem2  37919  finxp1o  37921  finxpreclem4  37923  finxp2o  37928  domalom  37933  onexoegt  43858  1oaomeqom  43907  oaabsb  43908  omnord1ex  43918  oaomoencom  43931  cantnftermord  43934  cantnf2  43939  omabs2  43946  omcl2  43947  1finon  44062  finona1cl  44066  1iscard  44155  hashnnsuc  45616