Theorem 1onn 8622

Description: The ordinal 1 is a natural number. For a shorter proof using Peano's postulates that depends on ax-un 7732, see 1onnALT 8623. Lemma 2.2 of [Schloeder] p. 4. (Contributed by NM, 29-Oct-1995.) Avoid ax-un 7732. (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 1825	. 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 1568   ∈ wcel 2143  Oncon0 6360  Lim wlim 6361  ω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 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-tr 5219  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  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  10281  cfpwsdom  10564  canthp1lem2  10633  gchdju1  10636  pwxpndom2  10645  pwdjundom  10647  1pi  10863  1lt2pi  10885  indpi  10887  hash2  14437  hash1snb  14452  fnpr2o  17606  fvpr1o  17609  f1otrspeq  19512  pmtrf  19520  pmtrmvd  19521  pmtrfinv  19526  lt6abl  19960  isnzr2  20615  frgpcyg  21723  vr1cl  22377  ply1coe  22458  isppw  27278  bnj906  35318  fineqvnttrclse  35537  sat1el2xp  35871  satfv1fvfmla1  35915  satefvfmla1  35917  ex-sategoelelomsuc  35918  ex-sategoelel12  35919  finxpreclem1  38035  finxpreclem2  38036  finxp1o  38038  finxpreclem4  38040  finxp2o  38045  domalom  38050  onexoegt  43971  1oaomeqom  44020  oaabsb  44021  omnord1ex  44031  oaomoencom  44044  cantnftermord  44047  cantnf2  44052  omabs2  44059  omcl2  44060  1finon  44175  finona1cl  44179  1iscard  44268  hashnnsuc  45729