Theorem 1onn 6731

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 6625	. 2 ⊢ 1o = suc ∅
2		peano1 4698	. . 3 ⊢ ∅ ∈ ω
3		peano2 4699	. . 3 ⊢ (∅ ∈ ω → suc ∅ ∈ ω)
4	2, 3	ax-mp 5	. 2 ⊢ suc ∅ ∈ ω
5	1, 4	eqeltri 2304	1 ⊢ 1o ∈ ω

Syntax hints:   ∈ wcel 2202  ∅c0 3496  suc csuc 4468  ωcom 4694  1_oc1o 6618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-nul 4220  ax-pow 4270  ax-pr 4305  ax-un 4536

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-nul 3497  df-pw 3658  df-sn 3679  df-pr 3680  df-uni 3899  df-int 3934  df-suc 4474  df-iom 4695  df-1o 6625

This theorem is referenced by:  2onn  6732  nnm2  6737  nnaordex  6739  snfig  7032  snnen2og  7088  1nen2  7090  1ndom2  7094  unfiexmid  7153  en1eqsn  7190  omp1eomlem  7336  fodjum  7388  fodju0  7389  nninfdcinf  7413  nninfwlporlemd  7414  nninfwlporlem  7415  en2eleq  7449  en2other2  7450  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  1pi  7578  1lt2pi  7603  archnqq  7680  nq0m0r  7719  nq02m  7728  prarloclemlt  7756  prarloclemlo  7757  1tonninf  10749  en1hash  11108  hash2  11122  fnpr2o  13485  fvpr1o  13488  upgrfi  16026  012of  16696  2omap  16698  pwle2  16703  peano3nninf  16716  nninfall  16718  nninfsellemdc  16719  nninfsellemeq  16723  nninfsellemeqinf  16725  nninffeq  16729  sbthom  16737  isomninnlem  16745  iswomninnlem  16765  ismkvnnlem  16768