Theorem 1onn 8607

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  Oncon0 6335  Lim wlim 6336  ωcom 7845  1_oc1o 8430

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-om 7846  df-1o 8437

This theorem is referenced by:  2onnALT  8610  1one2o  8613  oaabs2  8616  omabs  8618  nnm2  8620  nnneo  8622  nneob  8623  snfi  9017  snfiOLD  9018  1sdom2ALT  9195  1sdomOLD  9203  unxpdom2  9208  en1eqsnOLD  9227  wofib  9505  oancom  9611  cnfcom3clem  9665  ssttrcl  9675  ttrcltr  9676  djurf1o  9873  card1  9928  pm54.43lem  9960  en2eleq  9968  en2other2  9969  infxpenlem  9973  infxpenc2lem1  9979  sdom2en01  10262  cfpwsdom  10544  canthp1lem2  10613  gchdju1  10616  pwxpndom2  10625  pwdjundom  10627  1pi  10843  1lt2pi  10865  indpi  10867  hash2  14377  hash1snb  14391  fnpr2o  17527  fvpr1o  17530  f1otrspeq  19384  pmtrf  19392  pmtrmvd  19393  pmtrfinv  19398  lt6abl  19832  isnzr2  20434  frgpcyg  21490  vr1cl  22109  ply1coe  22192  isppw  27031  bnj906  34927  sat1el2xp  35373  satfv1fvfmla1  35417  satefvfmla1  35419  ex-sategoelelomsuc  35420  ex-sategoelel12  35421  finxpreclem1  37384  finxpreclem2  37385  finxp1o  37387  finxpreclem4  37389  finxp2o  37394  domalom  37399  onexoegt  43240  1oaomeqom  43289  oaabsb  43290  omnord1ex  43300  oaomoencom  43313  cantnftermord  43316  cantnf2  43321  omabs2  43328  omcl2  43329  1finon  43445  finona1cl  43449  1iscard  43538