Theorem 1onn 8594

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

Step	Hyp	Ref	Expression
1		1on 8434	. 2 ⊢ 1o ∈ On
2		1ellim 8451	. . 3 ⊢ (Lim 𝑥 → 1o ∈ 𝑥)
3	2	ax-gen 1805	. 2 ⊢ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)
4		elom 7834	. 2 ⊢ (1o ∈ ω ↔ (1o ∈ On ∧ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 719	1 ⊢ 1o ∈ ω

Syntax hints:   → wi 4  ∀wal 1548   ∈ wcel 2132  Oncon0 6331  Lim wlim 6332  ωcom 7831  1_oc1o 8414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pr 5380

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-pss 3915  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-tr 5198  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5589  df-we 5591  df-ord 6334  df-on 6335  df-lim 6336  df-suc 6337  df-om 7832  df-1o 8421

This theorem is referenced by:  2onnALT  8597  1one2o  8600  oaabs2  8603  omabs  8605  nnm2  8607  nnneo  8609  nneob  8610  snfi  9009  1sdom2ALT  9178  unxpdom2  9189  wofib  9479  oancom  9592  cnfcom3clem  9646  ssttrcl  9656  ttrcltr  9657  djurf1o  9857  card1  9912  pm54.43lem  9944  en2eleq  9950  en2other2  9951  infxpenlem  9955  infxpenc2lem1  9961  sdom2en01  10245  cfpwsdom  10528  canthp1lem2  10597  gchdju1  10600  pwxpndom2  10609  pwdjundom  10611  1pi  10827  1lt2pi  10849  indpi  10851  hash2  14404  hash1snb  14418  fnpr2o  17559  fvpr1o  17562  f1otrspeq  19459  pmtrf  19467  pmtrmvd  19468  pmtrfinv  19473  lt6abl  19907  isnzr2  20536  frgpcyg  21594  vr1cl  22248  ply1coe  22330  isppw  27144  bnj906  35172  fineqvnttrclse  35365  sat1el2xp  35667  satfv1fvfmla1  35711  satefvfmla1  35713  ex-sategoelelomsuc  35714  ex-sategoelel12  35715  finxpreclem1  37821  finxpreclem2  37822  finxp1o  37824  finxpreclem4  37826  finxp2o  37831  domalom  37836  onexoegt  43759  1oaomeqom  43808  oaabsb  43809  omnord1ex  43819  oaomoencom  43832  cantnftermord  43835  cantnf2  43840  omabs2  43847  omcl2  43848  1finon  43963  finona1cl  43967  1iscard  44056