Theorem 1onn 8628

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

Step	Hyp	Ref	Expression
1		1on 8468	. 2 ⊢ 1o ∈ On
2		1ellim 8485	. . 3 ⊢ (Lim 𝑥 → 1o ∈ 𝑥)
3	2	ax-gen 1828	. 2 ⊢ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)
4		elom 7865	. 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 6357  Lim wlim 6358  ωcom 7862  1_oc1o 8448

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-om 7863  df-1o 8455

This theorem is used by:  2onnALT  8631  1one2o  8634  oaabs2  8637  omabs  8639  nnm2  8641  nnneo  8643  nneob  8644  snfi  9050  1sdom2ALT  9219  unxpdom2  9230  wofib  9517  oancom  9630  cnfcom3clem  9684  ssttrcl  9694  ttrcltr  9695  djurf1o  9918  card1  9973  pm54.43lem  10005  en2eleq  10011  en2other2  10012  infxpenlem  10016  infxpenc2lem1  10022  sdom2en01  10304  cfpwsdom  10593  canthp1lem2  10662  gchdju1  10665  pwxpndom2  10674  pwdjundom  10676  1pi  10892  1lt2pi  10914  indpi  10916  hash2  14469  hash1snb  14484  fnpr2o  17643  fvpr1o  17646  f1otrspeq  19574  pmtrf  19582  pmtrmvd  19583  pmtrfinv  19588  lt6abl  20022  isnzr2  20678  frgpcyg  21786  vr1cl  22442  ply1coe  22523  isppw  27350  bnj906  35439  fineqvnttrclse  35650  sat1el2xp  35958  satfv1fvfmla1  36002  satefvfmla1  36004  ex-sategoelelomsuc  36005  ex-sategoelel12  36006  finxpreclem1  38143  finxpreclem2  38144  finxp1o  38146  finxpreclem4  38148  finxp2o  38153  domalom  38158  onexoegt  44085  1oaomeqom  44134  oaabsb  44135  omnord1ex  44145  oaomoencom  44158  cantnftermord  44161  cantnf2  44166  omabs2  44173  omcl2  44174  1finon  44289  finona1cl  44293  1iscard  44382  hashnnsuc  45843