Theorem 1onn 8581

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  Oncon0 6320  Lim wlim 6321  ωcom 7822  1_oc1o 8404

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 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-tr 5210  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-om 7823  df-1o 8411

This theorem is referenced by:  2onnALT  8584  1one2o  8587  oaabs2  8590  omabs  8592  nnm2  8594  nnneo  8596  nneob  8597  snfi  8991  snfiOLD  8992  1sdom2ALT  9165  1sdomOLD  9172  unxpdom2  9177  en1eqsnOLD  9196  wofib  9474  oancom  9580  cnfcom3clem  9634  ssttrcl  9644  ttrcltr  9645  djurf1o  9842  card1  9897  pm54.43lem  9929  en2eleq  9937  en2other2  9938  infxpenlem  9942  infxpenc2lem1  9948  sdom2en01  10231  cfpwsdom  10513  canthp1lem2  10582  gchdju1  10585  pwxpndom2  10594  pwdjundom  10596  1pi  10812  1lt2pi  10834  indpi  10836  hash2  14346  hash1snb  14360  fnpr2o  17496  fvpr1o  17499  f1otrspeq  19353  pmtrf  19361  pmtrmvd  19362  pmtrfinv  19367  lt6abl  19801  isnzr2  20403  frgpcyg  21459  vr1cl  22078  ply1coe  22161  isppw  27000  bnj906  34893  sat1el2xp  35339  satfv1fvfmla1  35383  satefvfmla1  35385  ex-sategoelelomsuc  35386  ex-sategoelel12  35387  finxpreclem1  37350  finxpreclem2  37351  finxp1o  37353  finxpreclem4  37355  finxp2o  37360  domalom  37365  onexoegt  43206  1oaomeqom  43255  oaabsb  43256  omnord1ex  43266  oaomoencom  43279  cantnftermord  43282  cantnf2  43287  omabs2  43294  omcl2  43295  1finon  43411  finona1cl  43415  1iscard  43504