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

Theorem 1nn 8371
Description: Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.)
Assertion
Ref Expression
1nn  |-  1  e.  NN

Proof of Theorem 1nn
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfnn2 8362 . . . 4  |-  NN  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }
21eleq2i 2151 . . 3  |-  ( 1  e.  NN  <->  1  e.  |^|
{ x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } )
3 1re 7434 . . . 4  |-  1  e.  RR
4 elintg 3681 . . . 4  |-  ( 1  e.  RR  ->  (
1  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }  <->  A. z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } 1  e.  z ) )
53, 4ax-mp 7 . . 3  |-  ( 1  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }  <->  A. z  e.  {
x  |  ( 1  e.  x  /\  A. y  e.  x  (
y  +  1 )  e.  x ) } 1  e.  z )
62, 5bitri 182 . 2  |-  ( 1  e.  NN  <->  A. z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } 1  e.  z )
7 vex 2618 . . . 4  |-  z  e. 
_V
8 eleq2 2148 . . . . 5  |-  ( x  =  z  ->  (
1  e.  x  <->  1  e.  z ) )
9 eleq2 2148 . . . . . 6  |-  ( x  =  z  ->  (
( y  +  1 )  e.  x  <->  ( y  +  1 )  e.  z ) )
109raleqbi1dv 2566 . . . . 5  |-  ( x  =  z  ->  ( A. y  e.  x  ( y  +  1 )  e.  x  <->  A. y  e.  z  ( y  +  1 )  e.  z ) )
118, 10anbi12d 457 . . . 4  |-  ( x  =  z  ->  (
( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x )  <-> 
( 1  e.  z  /\  A. y  e.  z  ( y  +  1 )  e.  z ) ) )
127, 11elab 2751 . . 3  |-  ( z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }  <->  ( 1  e.  z  /\  A. y  e.  z  ( y  +  1 )  e.  z ) )
1312simplbi 268 . 2  |-  ( z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }  ->  1  e.  z )
146, 13mprgbir 2429 1  |-  1  e.  NN
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103    e. wcel 1436   {cab 2071   A.wral 2355   |^|cint 3673  (class class class)co 5615   RRcr 7296   1c1 7298    + caddc 7300   NNcn 8360
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-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-1re 7386
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-ral 2360  df-v 2617  df-int 3674  df-inn 8361
This theorem is referenced by:  nnind  8376  nn1suc  8379  2nn  8514  1nn0  8625  nn0p1nn  8648  1z  8712  neg1z  8718  elz2  8754  nneoor  8784  9p1e10  8814  indstr  9016  elnn1uz2  9029  zq  9046  qreccl  9062  fz01or  9458  expivallem  9858  exp1  9863  nnexpcl  9870  expnbnd  9977  3dec  10023  fac1  10037  faccl  10043  faclbnd3  10051  resqrexlemf1  10340  resqrexlemcalc3  10348  resqrexlemnmsq  10349  resqrexlemnm  10350  resqrexlemcvg  10351  resqrexlemglsq  10354  resqrexlemga  10355  sumsnf  10691  n2dvds1  10818  ndvdsp1  10838  gcd1  10884  bezoutr1  10928  ncoprmgcdne1b  10977  1nprm  11002  1idssfct  11003  isprm2lem  11004  qden1elz  11089  phicl2  11096  phi1  11101  phiprm  11105
  Copyright terms: Public domain W3C validator