Theorem 1onn 8550

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

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

Step	Hyp	Ref	Expression
1		1on 8392	. 2 ⊢ 1o ∈ On
2		1ellim 8408	. . 3 ⊢ (Lim 𝑥 → 1o ∈ 𝑥)
3	2	ax-gen 1796	. 2 ⊢ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)
4		elom 7794	. 2 ⊢ (1o ∈ ω ↔ (1o ∈ On ∧ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥)))
5	1, 3, 4	mpbir2an 711	1 ⊢ 1o ∈ ω

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2111  Oncon0 6301  Lim wlim 6302  ωcom 7791  1_oc1o 8373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-om 7792  df-1o 8380

This theorem is referenced by:  2onnALT  8553  1one2o  8556  oaabs2  8559  omabs  8561  nnm2  8563  nnneo  8565  nneob  8566  snfi  8960  1sdom2ALT  9128  unxpdom2  9139  wofib  9426  oancom  9536  cnfcom3clem  9590  ssttrcl  9600  ttrcltr  9601  djurf1o  9801  card1  9856  pm54.43lem  9888  en2eleq  9894  en2other2  9895  infxpenlem  9899  infxpenc2lem1  9905  sdom2en01  10188  cfpwsdom  10470  canthp1lem2  10539  gchdju1  10542  pwxpndom2  10551  pwdjundom  10553  1pi  10769  1lt2pi  10791  indpi  10793  hash2  14307  hash1snb  14321  fnpr2o  17456  fvpr1o  17459  f1otrspeq  19354  pmtrf  19362  pmtrmvd  19363  pmtrfinv  19368  lt6abl  19802  isnzr2  20428  frgpcyg  21505  vr1cl  22125  ply1coe  22208  isppw  27046  bnj906  34934  fineqvnttrclse  35136  sat1el2xp  35415  satfv1fvfmla1  35459  satefvfmla1  35461  ex-sategoelelomsuc  35462  ex-sategoelel12  35463  finxpreclem1  37423  finxpreclem2  37424  finxp1o  37426  finxpreclem4  37428  finxp2o  37433  domalom  37438  onexoegt  43277  1oaomeqom  43326  oaabsb  43327  omnord1ex  43337  oaomoencom  43350  cantnftermord  43353  cantnf2  43358  omabs2  43365  omcl2  43366  1finon  43482  finona1cl  43486  1iscard  43575