ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  peano1 Structured version   Unicode version

Theorem peano1 4240
Description: Zero is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. (Contributed by NM, 15-May-1994.)
Assertion
Ref Expression
peano1  (/)  om

Proof of Theorem peano1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0ex 3854 . . . 4  (/)  _V
21elint 3591 . . 3  (/)  |^| {  |  (/) 
suc  }  {  |  (/) 
suc  }  (/)
3 df-clab 2005 . . . 4  {  |  (/) 
suc  }  (/)  suc
4 ax-ia1 99 . . . . . 6  (/)  suc 
(/)
54sbimi 1625 . . . . 5  (/)  suc  (/)
6 clelsb4 2121 . . . . 5  (/) 
(/)
75, 6sylib 127 . . . 4  (/)  suc  (/)
83, 7sylbi 114 . . 3  {  |  (/) 
suc  }  (/)
92, 8mpgbir 1318 . 2  (/)  |^| {  |  (/)  suc  }
10 dfom3 4238 . 2  om  |^|
{  |  (/)  suc  }
119, 10eleqtrri 2091 1  (/)  om
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wcel 1370  wsb 1623   {cab 2004  wral 2280   (/)c0 3197   |^|cint 3585   suc csuc 4047   omcom 4236
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-nul 3853
This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-v 2533  df-dif 2893  df-nul 3198  df-int 3586  df-iom 4237
This theorem is referenced by:  peano5  4244  limom  4259  nnregexmid  4265  frec0g  5898  frecrdg  5904  oa1suc  5958  nna0r  5968  nnm0r  5969  nnmcl  5971  nnmsucr  5978  1onn  6000  nnm1  6004  nnaordex  6007  nnawordex  6008  1lt2pi  6194  nq0m0r  6305  nq0a0  6306  prarloclem5  6348  peano5set  7301  bj-nn0suc  7321  bj-nn0sucALT  7335
  Copyright terms: Public domain W3C validator