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

Theorem peano1 4382
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 3941 . . . 4  |-  (/)  e.  _V
21elint 3677 . . 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 2072 . . . 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 107 . . . . . 6  |-  ( (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  (/)  e.  y )
54sbimi 1691 . . . . 5  |-  ( [ z  /  y ] ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  [ z  /  y ] (/)  e.  y )
6 clelsb4 2190 . . . . 5  |-  ( [ z  /  y ]
(/)  e.  y  <->  (/)  e.  z )
75, 6sylib 120 . . . 4  |-  ( [ z  /  y ] ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  (/)  e.  z )
83, 7sylbi 119 . . 3  |-  ( z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ->  (/)  e.  z )
92, 8mpgbir 1385 . 2  |-  (/)  e.  |^| { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }
10 dfom3 4380 . 2  |-  om  =  |^| { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }
119, 10eleqtrri 2160 1  |-  (/)  e.  om
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    e. wcel 1436   [wsb 1689   {cab 2071   A.wral 2355   (/)c0 3275   |^|cint 3671   suc csuc 4166   omcom 4378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-nul 3940
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-dif 2990  df-nul 3276  df-int 3672  df-iom 4379
This theorem is referenced by:  peano5  4386  limom  4401  nnregexmid  4407  omsinds  4408  frec0g  6116  frecabcl  6118  frecrdg  6127  oa1suc  6182  nna0r  6193  nnm0r  6194  nnmcl  6196  nnmsucr  6203  1onn  6231  nnm1  6235  nnaordex  6238  nnawordex  6239  php5  6526  php5dom  6531  0fin  6552  findcard2  6557  findcard2s  6558  infm  6572  inffiexmid  6574  fodjuomnilemm  6745  fodjuomnilem0  6746  1lt2pi  6843  nq0m0r  6959  nq0a0  6960  prarloclem5  7003  frec2uzrand  9740  frecuzrdg0  9748  frecuzrdg0t  9757  frecfzennn  9761  0tonninf  9773  1tonninf  9774  hashinfom  10082  hashunlem  10108  hash1  10115  bj-nn0suc  11297  bj-nn0sucALT  11311  nnpredcl  11328  peano3nninf  11335  nninfall  11338  nninfsellemdc  11340  nninfsellemeq  11344
  Copyright terms: Public domain W3C validator