Theorem 1onn 8558

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  Oncon0 6307  Lim wlim 6308  ωcom 7799  1_oc1o 8381

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-tr 5200  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-om 7800  df-1o 8388

This theorem is referenced by:  2onnALT  8561  1one2o  8564  oaabs2  8567  omabs  8569  nnm2  8571  nnneo  8573  nneob  8574  snfi  8968  snfiOLD  8969  1sdom2ALT  9138  unxpdom2  9149  wofib  9437  oancom  9547  cnfcom3clem  9601  ssttrcl  9611  ttrcltr  9612  djurf1o  9809  card1  9864  pm54.43lem  9896  en2eleq  9902  en2other2  9903  infxpenlem  9907  infxpenc2lem1  9913  sdom2en01  10196  cfpwsdom  10478  canthp1lem2  10547  gchdju1  10550  pwxpndom2  10559  pwdjundom  10561  1pi  10777  1lt2pi  10799  indpi  10801  hash2  14312  hash1snb  14326  fnpr2o  17461  fvpr1o  17464  f1otrspeq  19326  pmtrf  19334  pmtrmvd  19335  pmtrfinv  19340  lt6abl  19774  isnzr2  20403  frgpcyg  21480  vr1cl  22100  ply1coe  22183  isppw  27022  bnj906  34897  sat1el2xp  35352  satfv1fvfmla1  35396  satefvfmla1  35398  ex-sategoelelomsuc  35399  ex-sategoelel12  35400  finxpreclem1  37363  finxpreclem2  37364  finxp1o  37366  finxpreclem4  37368  finxp2o  37373  domalom  37378  onexoegt  43217  1oaomeqom  43266  oaabsb  43267  omnord1ex  43277  oaomoencom  43290  cantnftermord  43293  cantnf2  43298  omabs2  43305  omcl2  43306  1finon  43422  finona1cl  43426  1iscard  43515