Theorem 1onn 8654

Description: The ordinal 1 is a natural number. For a shorter proof using Peano's postulates that depends on ax-un 7753, see 1onnALT 8655. 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 8494	. 2 ⊢ 1o ∈ On
2		1ellim 8511	. . 3 ⊢ (Lim 𝑥 → 1o ∈ 𝑥)
3	2	ax-gen 1827	. 2 ⊢ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)
4		elom 7882	. 2 ⊢ (1o ∈ ω ↔ (1o ∈ On ∧ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 724	1 ⊢ 1o ∈ ω

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   ∈ wcel 2144  Oncon0 6364  Lim wlim 6365  ωcom 7879  1_oc1o 8474

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-om 7880  df-1o 8481

This theorem is used by:  2onnALT  8657  1one2o  8660  oaabs2  8663  omabs  8665  nnm2  8667  nnneo  8669  nneob  8670  snfi  9076  1sdom2ALT  9245  unxpdom2  9256  wofib  9544  oancom  9657  cnfcom3clem  9711  ssttrcl  9721  ttrcltr  9722  djurf1o  9999  card1  10054  pm54.43lem  10086  en2eleq  10092  en2other2  10093  infxpenlem  10097  infxpenc2lem1  10103  sdom2en01  10385  cfpwsdom  10674  canthp1lem2  10743  gchdju1  10746  pwxpndom2  10755  pwdjundom  10757  1pi  10973  1lt2pi  10995  indpi  10997  hash2  14554  hash1snb  14569  fnpr2o  17736  fvpr1o  17739  f1otrspeq  19668  pmtrf  19676  pmtrmvd  19677  pmtrfinv  19682  lt6abl  20116  isnzr2  20775  frgpcyg  21886  vr1cl  22542  ply1coe  22623  isppw  27448  bnj906  35608  fineqvnttrclse  35850  sat1el2xp  36232  satfv1fvfmla1  36276  satefvfmla1  36278  ex-sategoelelomsuc  36279  ex-sategoelel12  36280  finxpreclem1  38419  finxpreclem2  38420  finxp1o  38422  finxpreclem4  38424  finxp2o  38429  domalom  38434  onexoegt  44353  1oaomeqom  44402  oaabsb  44403  omnord1ex  44413  oaomoencom  44426  cantnftermord  44429  cantnf2  44434  omabs2  44441  omcl2  44442  1finon  44557  finona1cl  44561  1iscard  44650  hashnnsuc  46117