Theorem 1onn 8642

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

Step	Hyp	Ref	Expression
1		1on 8482	. 2 ⊢ 1o ∈ On
2		1ellim 8499	. . 3 ⊢ (Lim 𝑥 → 1o ∈ 𝑥)
3	2	ax-gen 1828	. 2 ⊢ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)
4		elom 7878	. 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 2145  Oncon0 6361  Lim wlim 6362  ωcom 7875  1_oc1o 8462

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-om 7876  df-1o 8469

This theorem is used by:  2onnALT  8645  1one2o  8648  oaabs2  8651  omabs  8653  nnm2  8655  nnneo  8657  nneob  8658  snfi  9064  1sdom2ALT  9233  unxpdom2  9244  wofib  9532  oancom  9645  cnfcom3clem  9699  ssttrcl  9709  ttrcltr  9710  djurf1o  9987  card1  10042  pm54.43lem  10074  en2eleq  10080  en2other2  10081  infxpenlem  10085  infxpenc2lem1  10091  sdom2en01  10373  cfpwsdom  10662  canthp1lem2  10731  gchdju1  10734  pwxpndom2  10743  pwdjundom  10745  1pi  10961  1lt2pi  10983  indpi  10985  hash2  14542  hash1snb  14557  fnpr2o  17722  fvpr1o  17725  f1otrspeq  19654  pmtrf  19662  pmtrmvd  19663  pmtrfinv  19668  lt6abl  20102  isnzr2  20761  frgpcyg  21872  vr1cl  22528  ply1coe  22609  isppw  27434  bnj906  35553  fineqvnttrclse  35775  sat1el2xp  36123  satfv1fvfmla1  36167  satefvfmla1  36169  ex-sategoelelomsuc  36170  ex-sategoelel12  36171  finxpreclem1  38292  finxpreclem2  38293  finxp1o  38295  finxpreclem4  38297  finxp2o  38302  domalom  38307  onexoegt  44230  1oaomeqom  44279  oaabsb  44280  omnord1ex  44290  oaomoencom  44303  cantnftermord  44306  cantnf2  44311  omabs2  44318  omcl2  44319  1finon  44434  finona1cl  44438  1iscard  44527  hashnnsuc  45988