Theorem 1onn 7874

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

Assertion

Ref	Expression
1onn	⊢ 1𝑜 ∈ ω

Proof of Theorem 1onn

Step	Hyp	Ref	Expression
1		df-1o 7714	. 2 ⊢ 1𝑜 = suc ∅
2		peano1 7233	. . 3 ⊢ ∅ ∈ ω
3		peano2 7234	. . 3 ⊢ (∅ ∈ ω → suc ∅ ∈ ω)
4	2, 3	ax-mp 5	. 2 ⊢ suc ∅ ∈ ω
5	1, 4	eqeltri 2846	1 ⊢ 1𝑜 ∈ ω

Syntax hints:   ∈ wcel 2145  ∅c0 4064  suc csuc 5869  ωcom 7213  1_𝑜c1o 7707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035  ax-un 7097

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3589  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-tr 4888  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-om 7214  df-1o 7714

This theorem is referenced by:  2onn  7875  oaabs2  7880  omabs  7882  nnm2  7884  nnneo  7886  nneob  7887  snfi  8195  snnen2o  8306  1sdom2  8316  1sdom  8320  unxpdom2  8325  en1eqsn  8347  en2  8353  pwfi  8418  wofib  8607  oancom  8713  cnfcom3clem  8767  djurcl  8938  djurf1o  8940  djuun  8953  card1  8995  pm54.43lem  9026  en2eleq  9032  en2other2  9033  infxpenlem  9037  infxpenc2lem1  9043  infmap2  9243  sdom2en01  9327  cfpwsdom  9609  canthp1lem2  9678  gchcda1  9681  pwxpndom2  9690  pwcdandom  9692  1pi  9908  1lt2pi  9930  indpi  9932  hash2  13396  hash1snb  13410  setcepi  16946  f1otrspeq  18075  pmtrf  18083  pmtrmvd  18084  pmtrfinv  18089  lt6abl  18504  isnzr2  19479  vr1cl  19803  ply1coe  19882  frgpcyg  20138  isppw  25062  bnj906  31339  finxpreclem1  33564  finxpreclem2  33565  finxp1o  33567  finxpreclem4  33569  finxp2o  33574