Theorem 1onn 8632

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

Step	Hyp	Ref	Expression
1		1on 8472	. 2 ⊢ 1o ∈ On
2		1ellim 8489	. . 3 ⊢ (Lim 𝑥 → 1o ∈ 𝑥)
3	2	ax-gen 1828	. 2 ⊢ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)
4		elom 7871	. 2 ⊢ (1o ∈ ω ↔ (1o ∈ On ∧ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 724	1 ⊢ 1o ∈ ω

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2146  Oncon0 6364  Lim wlim 6365  ωcom 7868  1_oc1o 8452

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-om 7869  df-1o 8459

This theorem is used by:  2onnALT  8635  1one2o  8638  oaabs2  8641  omabs  8643  nnm2  8645  nnneo  8647  nneob  8648  snfi  9047  1sdom2ALT  9216  unxpdom2  9227  wofib  9514  oancom  9627  cnfcom3clem  9681  ssttrcl  9691  ttrcltr  9692  djurf1o  9915  card1  9970  pm54.43lem  10002  en2eleq  10008  en2other2  10009  infxpenlem  10013  infxpenc2lem1  10019  sdom2en01  10301  cfpwsdom  10584  canthp1lem2  10653  gchdju1  10656  pwxpndom2  10665  pwdjundom  10667  1pi  10883  1lt2pi  10905  indpi  10907  hash2  14459  hash1snb  14474  fnpr2o  17633  fvpr1o  17636  f1otrspeq  19561  pmtrf  19569  pmtrmvd  19570  pmtrfinv  19575  lt6abl  20009  isnzr2  20665  frgpcyg  21773  vr1cl  22427  ply1coe  22508  isppw  27329  bnj906  35383  fineqvnttrclse  35594  sat1el2xp  35908  satfv1fvfmla1  35952  satefvfmla1  35954  ex-sategoelelomsuc  35955  ex-sategoelel12  35956  finxpreclem1  38092  finxpreclem2  38093  finxp1o  38095  finxpreclem4  38097  finxp2o  38102  domalom  38107  onexoegt  44029  1oaomeqom  44078  oaabsb  44079  omnord1ex  44089  oaomoencom  44102  cantnftermord  44105  cantnf2  44110  omabs2  44117  omcl2  44118  1finon  44233  finona1cl  44237  1iscard  44326  hashnnsuc  45787