Theorem 1onn 8569

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

Step	Hyp	Ref	Expression
1		1on 8410	. 2 ⊢ 1o ∈ On
2		1ellim 8426	. . 3 ⊢ (Lim 𝑥 → 1o ∈ 𝑥)
3	2	ax-gen 1797	. 2 ⊢ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)
4		elom 7813	. 2 ⊢ (1o ∈ ω ↔ (1o ∈ On ∧ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 712	1 ⊢ 1o ∈ ω

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  Oncon0 6317  Lim wlim 6318  ωcom 7810  1_oc1o 8391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-om 7811  df-1o 8398

This theorem is referenced by:  2onnALT  8572  1one2o  8575  oaabs2  8578  omabs  8580  nnm2  8582  nnneo  8584  nneob  8585  snfi  8983  1sdom2ALT  9152  unxpdom2  9163  wofib  9453  oancom  9563  cnfcom3clem  9617  ssttrcl  9627  ttrcltr  9628  djurf1o  9828  card1  9883  pm54.43lem  9915  en2eleq  9921  en2other2  9922  infxpenlem  9926  infxpenc2lem1  9932  sdom2en01  10215  cfpwsdom  10498  canthp1lem2  10567  gchdju1  10570  pwxpndom2  10579  pwdjundom  10581  1pi  10797  1lt2pi  10819  indpi  10821  hash2  14358  hash1snb  14372  fnpr2o  17512  fvpr1o  17515  f1otrspeq  19413  pmtrf  19421  pmtrmvd  19422  pmtrfinv  19427  lt6abl  19861  isnzr2  20486  frgpcyg  21563  vr1cl  22191  ply1coe  22273  isppw  27091  bnj906  35088  fineqvnttrclse  35284  sat1el2xp  35577  satfv1fvfmla1  35621  satefvfmla1  35623  ex-sategoelelomsuc  35624  ex-sategoelel12  35625  finxpreclem1  37719  finxpreclem2  37720  finxp1o  37722  finxpreclem4  37724  finxp2o  37729  domalom  37734  onexoegt  43690  1oaomeqom  43739  oaabsb  43740  omnord1ex  43750  oaomoencom  43763  cantnftermord  43766  cantnf2  43771  omabs2  43778  omcl2  43779  1finon  43894  finona1cl  43898  1iscard  43987