Theorem 1onn 8566

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

Step	Hyp	Ref	Expression
1		1on 8407	. 2 ⊢ 1o ∈ On
2		1ellim 8423	. . 3 ⊢ (Lim 𝑥 → 1o ∈ 𝑥)
3	2	ax-gen 1802	. 2 ⊢ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)
4		elom 7809	. 2 ⊢ (1o ∈ ω ↔ (1o ∈ On ∧ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 717	1 ⊢ 1o ∈ ω

Syntax hints:   → wi 4  ∀wal 1545   ∈ wcel 2119  Oncon0 6310  Lim wlim 6311  ωcom 7806  1_oc1o 8388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-tr 5180  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-om 7807  df-1o 8395

This theorem is referenced by:  2onnALT  8569  1one2o  8572  oaabs2  8575  omabs  8577  nnm2  8579  nnneo  8581  nneob  8582  snfi  8980  1sdom2ALT  9149  unxpdom2  9160  wofib  9450  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  20490  frgpcyg  21548  vr1cl  22202  ply1coe  22284  isppw  27095  bnj906  35112  fineqvnttrclse  35305  sat1el2xp  35607  satfv1fvfmla1  35651  satefvfmla1  35653  ex-sategoelelomsuc  35654  ex-sategoelel12  35655  finxpreclem1  37751  finxpreclem2  37752  finxp1o  37754  finxpreclem4  37756  finxp2o  37761  domalom  37766  onexoegt  43689  1oaomeqom  43738  oaabsb  43739  omnord1ex  43749  oaomoencom  43762  cantnftermord  43765  cantnf2  43770  omabs2  43777  omcl2  43778  1finon  43893  finona1cl  43897  1iscard  43986