Theorem 1onn 8005

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 7845	. 2 ⊢ 1o = suc ∅
2		peano1 7365	. . 3 ⊢ ∅ ∈ ω
3		peano2 7366	. . 3 ⊢ (∅ ∈ ω → suc ∅ ∈ ω)
4	2, 3	ax-mp 5	. 2 ⊢ suc ∅ ∈ ω
5	1, 4	eqeltri 2855	1 ⊢ 1o ∈ ω

Syntax hints:   ∈ wcel 2107  ∅c0 4141  suc csuc 5980  ωcom 7345  1_oc1o 7838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pr 5140  ax-un 7228

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-tr 4990  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-om 7346  df-1o 7845

This theorem is referenced by:  2onn  8006  oaabs2  8011  omabs  8013  nnm2  8015  nnneo  8017  nneob  8018  snfi  8328  snnen2o  8439  1sdom2  8449  1sdom  8453  unxpdom2  8458  en1eqsn  8480  en2  8486  pwfi  8551  wofib  8741  oancom  8847  cnfcom3clem  8901  djurf1o  9074  card1  9129  pm54.43lem  9160  en2eleq  9166  en2other2  9167  infxpenlem  9171  infxpenc2lem1  9177  sdom2en01  9461  cfpwsdom  9743  canthp1lem2  9812  gchcda1  9815  pwxpndom2  9824  pwcdandom  9826  1pi  10042  1lt2pi  10064  indpi  10066  hash2  13511  hash1snb  13525  f1otrspeq  18254  pmtrf  18262  pmtrmvd  18263  pmtrfinv  18268  lt6abl  18686  isnzr2  19664  vr1cl  19987  ply1coe  20066  frgpcyg  20321  isppw  25296  bnj906  31603  finxpreclem1  33824  finxpreclem2  33825  finxp1o  33827  finxpreclem4  33829  finxp2o  33834