Theorem 1onn 8564

Description: The ordinal 1 is a natural number. For a shorter proof using Peano's postulates that depends on ax-un 7677, see 1onnALT 8565. 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 8406	. 2 ⊢ 1o ∈ On
2		1ellim 8422	. . 3 ⊢ (Lim 𝑥 → 1o ∈ 𝑥)
3	2	ax-gen 1796	. 2 ⊢ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)
4		elom 7808	. 2 ⊢ (1o ∈ ω ↔ (1o ∈ On ∧ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 711	1 ⊢ 1o ∈ ω

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113  Oncon0 6314  Lim wlim 6315  ωcom 7805  1_oc1o 8387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-om 7806  df-1o 8394

This theorem is referenced by:  2onnALT  8567  1one2o  8570  oaabs2  8573  omabs  8575  nnm2  8577  nnneo  8579  nneob  8580  snfi  8976  1sdom2ALT  9144  unxpdom2  9155  wofib  9442  oancom  9552  cnfcom3clem  9606  ssttrcl  9616  ttrcltr  9617  djurf1o  9817  card1  9872  pm54.43lem  9904  en2eleq  9910  en2other2  9911  infxpenlem  9915  infxpenc2lem1  9921  sdom2en01  10204  cfpwsdom  10486  canthp1lem2  10555  gchdju1  10558  pwxpndom2  10567  pwdjundom  10569  1pi  10785  1lt2pi  10807  indpi  10809  hash2  14319  hash1snb  14333  fnpr2o  17469  fvpr1o  17472  f1otrspeq  19367  pmtrf  19375  pmtrmvd  19376  pmtrfinv  19381  lt6abl  19815  isnzr2  20442  frgpcyg  21519  vr1cl  22149  ply1coe  22233  isppw  27071  bnj906  35014  fineqvnttrclse  35216  sat1el2xp  35495  satfv1fvfmla1  35539  satefvfmla1  35541  ex-sategoelelomsuc  35542  ex-sategoelel12  35543  finxpreclem1  37506  finxpreclem2  37507  finxp1o  37509  finxpreclem4  37511  finxp2o  37516  domalom  37521  onexoegt  43401  1oaomeqom  43450  oaabsb  43451  omnord1ex  43461  oaomoencom  43474  cantnftermord  43477  cantnf2  43482  omabs2  43489  omcl2  43490  1finon  43606  finona1cl  43610  1iscard  43699