Theorem 1onn 8591

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2106  Oncon0 6322  Lim wlim 6323  ωcom 7807  1_oc1o 8410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-tr 5228  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-om 7808  df-1o 8417

This theorem is referenced by:  2onnALT  8594  1one2o  8597  oaabs2  8600  omabs  8602  nnm2  8604  nnneo  8606  nneob  8607  snfi  8995  snnen2oOLD  9178  1sdom2ALT  9192  1sdomOLD  9200  unxpdom2  9205  en1eqsnOLD  9226  pwfiOLD  9298  wofib  9490  oancom  9596  cnfcom3clem  9650  ssttrcl  9660  ttrcltr  9661  djurf1o  9858  card1  9913  pm54.43lem  9945  en2eleq  9953  en2other2  9954  infxpenlem  9958  infxpenc2lem1  9964  sdom2en01  10247  cfpwsdom  10529  canthp1lem2  10598  gchdju1  10601  pwxpndom2  10610  pwdjundom  10612  1pi  10828  1lt2pi  10850  indpi  10852  hash2  14315  hash1snb  14329  fnpr2o  17453  fvpr1o  17456  f1otrspeq  19243  pmtrf  19251  pmtrmvd  19252  pmtrfinv  19257  lt6abl  19686  isnzr2  20207  frgpcyg  21017  vr1cl  21625  ply1coe  21704  isppw  26500  bnj906  33631  sat1el2xp  34060  satfv1fvfmla1  34104  satefvfmla1  34106  ex-sategoelelomsuc  34107  ex-sategoelel12  34108  finxpreclem1  35933  finxpreclem2  35934  finxp1o  35936  finxpreclem4  35938  finxp2o  35943  domalom  35948  onexoegt  41636  1oaomeqom  41686  oaabsb  41687  omnord1ex  41697  oaomoencom  41710  cantnftermord  41713  cantnf2  41718  omabs2  41725  omcl2  41726  1finon  41843  finona1cl  41847  1iscard  41936