Theorem 1onn 8657

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  Oncon0 6357  Lim wlim 6358  ωcom 7866  1_oc1o 8478

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-tr 5235  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-om 7867  df-1o 8485

This theorem is referenced by:  2onnALT  8660  1one2o  8663  oaabs2  8666  omabs  8668  nnm2  8670  nnneo  8672  nneob  8673  snfi  9062  snfiOLD  9063  snnen2oOLD  9241  1sdom2ALT  9254  1sdomOLD  9262  unxpdom2  9267  en1eqsnOLD  9286  wofib  9564  oancom  9670  cnfcom3clem  9724  ssttrcl  9734  ttrcltr  9735  djurf1o  9932  card1  9987  pm54.43lem  10019  en2eleq  10027  en2other2  10028  infxpenlem  10032  infxpenc2lem1  10038  sdom2en01  10321  cfpwsdom  10603  canthp1lem2  10672  gchdju1  10675  pwxpndom2  10684  pwdjundom  10686  1pi  10902  1lt2pi  10924  indpi  10926  hash2  14428  hash1snb  14442  fnpr2o  17576  fvpr1o  17579  f1otrspeq  19433  pmtrf  19441  pmtrmvd  19442  pmtrfinv  19447  lt6abl  19881  isnzr2  20483  frgpcyg  21539  vr1cl  22158  ply1coe  22241  isppw  27081  bnj906  34966  sat1el2xp  35406  satfv1fvfmla1  35450  satefvfmla1  35452  ex-sategoelelomsuc  35453  ex-sategoelel12  35454  finxpreclem1  37412  finxpreclem2  37413  finxp1o  37415  finxpreclem4  37417  finxp2o  37422  domalom  37427  onexoegt  43235  1oaomeqom  43284  oaabsb  43285  omnord1ex  43295  oaomoencom  43308  cantnftermord  43311  cantnf2  43316  omabs2  43323  omcl2  43324  1finon  43440  finona1cl  43444  1iscard  43533