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

Theorem peano1 4478
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  |-  (/)  e.  om

Proof of Theorem peano1
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0ex 4025 . . . 4  |-  (/)  e.  _V
21elint 3747 . . 3  |-  ( (/)  e.  |^| { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  <->  A. z
( z  e.  {
y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ->  (/)  e.  z ) )
3 df-clab 2104 . . . 4  |-  ( z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  <->  [ z  /  y ] (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) )
4 simpl 108 . . . . . 6  |-  ( (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  (/)  e.  y )
54sbimi 1722 . . . . 5  |-  ( [ z  /  y ] ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  [ z  /  y ] (/)  e.  y )
6 clelsb4 2223 . . . . 5  |-  ( [ z  /  y ]
(/)  e.  y  <->  (/)  e.  z )
75, 6sylib 121 . . . 4  |-  ( [ z  /  y ] ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  (/)  e.  z )
83, 7sylbi 120 . . 3  |-  ( z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ->  (/)  e.  z )
92, 8mpgbir 1414 . 2  |-  (/)  e.  |^| { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }
10 dfom3 4476 . 2  |-  om  =  |^| { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }
119, 10eleqtrri 2193 1  |-  (/)  e.  om
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 1465   [wsb 1720   {cab 2103   A.wral 2393   (/)c0 3333   |^|cint 3741   suc csuc 4257   omcom 4474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-nul 4024
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-dif 3043  df-nul 3334  df-int 3742  df-iom 4475
This theorem is referenced by:  peano5  4482  limom  4497  nnregexmid  4504  omsinds  4505  nnpredcl  4506  frec0g  6262  frecabcl  6264  frecrdg  6273  oa1suc  6331  nna0r  6342  nnm0r  6343  nnmcl  6345  nnmsucr  6352  1onn  6384  nnm1  6388  nnaordex  6391  nnawordex  6392  php5  6720  php5dom  6725  0fin  6746  findcard2  6751  findcard2s  6752  infm  6766  inffiexmid  6768  0ct  6960  ctmlemr  6961  ctssdclemn0  6963  ctssdc  6966  omct  6970  fodjum  6986  fodju0  6987  ctssexmid  6992  1lt2pi  7116  nq0m0r  7232  nq0a0  7233  prarloclem5  7276  frec2uzrand  10146  frecuzrdg0  10154  frecuzrdg0t  10163  frecfzennn  10167  0tonninf  10180  1tonninf  10181  hashinfom  10492  hashunlem  10518  hash1  10525  ennnfonelemj0  11841  ennnfonelem1  11847  ennnfonelemhf1o  11853  ennnfonelemhom  11855  bj-nn0suc  13089  bj-nn0sucALT  13103  pwle2  13120  pwf1oexmid  13121  subctctexmid  13123  peano3nninf  13128  nninfall  13131  nninfsellemdc  13133  nninfsellemeq  13137  nninffeq  13143  isomninnlem  13152
  Copyright terms: Public domain W3C validator