Theorem 1onn 8576

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  Oncon0 6323  Lim wlim 6324  ωcom 7817  1_oc1o 8398

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-tr 5193  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-om 7818  df-1o 8405

This theorem is referenced by:  2onnALT  8579  1one2o  8582  oaabs2  8585  omabs  8587  nnm2  8589  nnneo  8591  nneob  8592  snfi  8990  1sdom2ALT  9159  unxpdom2  9170  wofib  9460  oancom  9572  cnfcom3clem  9626  ssttrcl  9636  ttrcltr  9637  djurf1o  9837  card1  9892  pm54.43lem  9924  en2eleq  9930  en2other2  9931  infxpenlem  9935  infxpenc2lem1  9941  sdom2en01  10224  cfpwsdom  10507  canthp1lem2  10576  gchdju1  10579  pwxpndom2  10588  pwdjundom  10590  1pi  10806  1lt2pi  10828  indpi  10830  hash2  14367  hash1snb  14381  fnpr2o  17521  fvpr1o  17524  f1otrspeq  19422  pmtrf  19430  pmtrmvd  19431  pmtrfinv  19436  lt6abl  19870  isnzr2  20495  frgpcyg  21553  vr1cl  22181  ply1coe  22263  isppw  27077  bnj906  35072  fineqvnttrclse  35268  sat1el2xp  35561  satfv1fvfmla1  35605  satefvfmla1  35607  ex-sategoelelomsuc  35608  ex-sategoelel12  35609  finxpreclem1  37705  finxpreclem2  37706  finxp1o  37708  finxpreclem4  37710  finxp2o  37715  domalom  37720  onexoegt  43672  1oaomeqom  43721  oaabsb  43722  omnord1ex  43732  oaomoencom  43745  cantnftermord  43748  cantnf2  43753  omabs2  43760  omcl2  43761  1finon  43876  finona1cl  43880  1iscard  43969