Theorem 1onn 8446

Description: One is a natural number. (Contributed by NM, 29-Oct-1995.)

Assertion

Ref	Expression
1onn	⊢ 1o ∈ ω

Proof of Theorem 1onn

Step	Hyp	Ref	Expression
1		df-1o 8281	. 2 ⊢ 1o = suc ∅
2		peano1 7723	. . 3 ⊢ ∅ ∈ ω
3		peano2 7724	. . 3 ⊢ (∅ ∈ ω → suc ∅ ∈ ω)
4	2, 3	ax-mp 5	. 2 ⊢ suc ∅ ∈ ω
5	1, 4	eqeltri 2836	1 ⊢ 1o ∈ ω

Syntax hints:   ∈ wcel 2109  ∅c0 4261  suc csuc 6265  ωcom 7700  1_oc1o 8274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-11 2157  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-tr 5196  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-om 7701  df-1o 8281

This theorem is referenced by:  2onn  8447  1one2o  8450  oaabs2  8453  omabs  8455  nnm2  8457  nnneo  8459  nneob  8460  snfi  8804  snnen2o  8963  1sdom2  8983  1sdom  8987  unxpdom2  8992  en1eqsn  9009  en2  9014  pwfiOLD  9075  wofib  9265  oancom  9370  cnfcom3clem  9424  ssttrcl  9434  ttrcltr  9435  djurf1o  9655  card1  9710  pm54.43lem  9742  en2eleq  9748  en2other2  9749  infxpenlem  9753  infxpenc2lem1  9759  sdom2en01  10042  cfpwsdom  10324  canthp1lem2  10393  gchdju1  10396  pwxpndom2  10405  pwdjundom  10407  1pi  10623  1lt2pi  10645  indpi  10647  hash2  14101  hash1snb  14115  fnpr2o  17249  fvpr1o  17252  f1otrspeq  19036  pmtrf  19044  pmtrmvd  19045  pmtrfinv  19050  lt6abl  19477  isnzr2  20515  frgpcyg  20762  vr1cl  21369  ply1coe  21448  isppw  26244  bnj906  32889  sat1el2xp  33320  satfv1fvfmla1  33364  satefvfmla1  33366  ex-sategoelelomsuc  33367  ex-sategoelel12  33368  finxpreclem1  35539  finxpreclem2  35540  finxp1o  35542  finxpreclem4  35544  finxp2o  35549  domalom  35554