Theorem 1onn 8661

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

Step	Hyp	Ref	Expression
1		1on 8499	. 2 ⊢ 1o ∈ On
2		1ellim 8519	. . 3 ⊢ (Lim 𝑥 → 1o ∈ 𝑥)
3	2	ax-gen 1789	. 2 ⊢ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)
4		elom 7874	. 2 ⊢ (1o ∈ ω ↔ (1o ∈ On ∧ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 709	1 ⊢ 1o ∈ ω

Syntax hints:   → wi 4  ∀wal 1531   ∈ wcel 2098  Oncon0 6371  Lim wlim 6372  ωcom 7871  1_oc1o 8480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-om 7872  df-1o 8487

This theorem is referenced by:  2onnALT  8664  1one2o  8667  oaabs2  8670  omabs  8672  nnm2  8674  nnneo  8676  nneob  8677  snfi  9069  snnen2oOLD  9252  1sdom2ALT  9266  1sdomOLD  9274  unxpdom2  9279  en1eqsnOLD  9300  pwfiOLD  9373  wofib  9570  oancom  9676  cnfcom3clem  9730  ssttrcl  9740  ttrcltr  9741  djurf1o  9938  card1  9993  pm54.43lem  10025  en2eleq  10033  en2other2  10034  infxpenlem  10038  infxpenc2lem1  10044  sdom2en01  10327  cfpwsdom  10609  canthp1lem2  10678  gchdju1  10681  pwxpndom2  10690  pwdjundom  10692  1pi  10908  1lt2pi  10930  indpi  10932  hash2  14400  hash1snb  14414  fnpr2o  17542  fvpr1o  17545  f1otrspeq  19414  pmtrf  19422  pmtrmvd  19423  pmtrfinv  19428  lt6abl  19862  isnzr2  20469  frgpcyg  21524  vr1cl  22160  ply1coe  22242  isppw  27091  bnj906  34689  sat1el2xp  35117  satfv1fvfmla1  35161  satefvfmla1  35163  ex-sategoelelomsuc  35164  ex-sategoelel12  35165  finxpreclem1  36996  finxpreclem2  36997  finxp1o  36999  finxpreclem4  37001  finxp2o  37006  domalom  37011  onexoegt  42811  1oaomeqom  42861  oaabsb  42862  omnord1ex  42872  oaomoencom  42885  cantnftermord  42888  cantnf2  42893  omabs2  42900  omcl2  42901  1finon  43018  finona1cl  43022  1iscard  43111