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

Theorem peano2nn 8929
Description: Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
peano2nn  |-  ( A  e.  NN  ->  ( A  +  1 )  e.  NN )

Proof of Theorem peano2nn
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfnn2 8919 . . . . . 6  |-  NN  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }
21eleq2i 2244 . . . . 5  |-  ( A  e.  NN  <->  A  e.  |^|
{ x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } )
3 elintg 3852 . . . . 5  |-  ( A  e.  NN  ->  ( A  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 ) } A  e.  z ) )
42, 3bitrid 192 . . . 4  |-  ( A  e.  NN  ->  ( A  e.  NN  <->  A. z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } A  e.  z ) )
54ibi 176 . . 3  |-  ( A  e.  NN  ->  A. z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } A  e.  z )
6 vex 2740 . . . . . . . 8  |-  z  e. 
_V
7 eleq2 2241 . . . . . . . . 9  |-  ( x  =  z  ->  (
1  e.  x  <->  1  e.  z ) )
8 eleq2 2241 . . . . . . . . . 10  |-  ( x  =  z  ->  (
( y  +  1 )  e.  x  <->  ( y  +  1 )  e.  z ) )
98raleqbi1dv 2680 . . . . . . . . 9  |-  ( x  =  z  ->  ( A. y  e.  x  ( y  +  1 )  e.  x  <->  A. y  e.  z  ( y  +  1 )  e.  z ) )
107, 9anbi12d 473 . . . . . . . 8  |-  ( x  =  z  ->  (
( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x )  <-> 
( 1  e.  z  /\  A. y  e.  z  ( y  +  1 )  e.  z ) ) )
116, 10elab 2881 . . . . . . 7  |-  ( 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 ) )
1211simprbi 275 . . . . . 6  |-  ( z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }  ->  A. y  e.  z  ( y  +  1 )  e.  z )
13 oveq1 5881 . . . . . . . 8  |-  ( y  =  A  ->  (
y  +  1 )  =  ( A  + 
1 ) )
1413eleq1d 2246 . . . . . . 7  |-  ( y  =  A  ->  (
( y  +  1 )  e.  z  <->  ( A  +  1 )  e.  z ) )
1514rspcva 2839 . . . . . 6  |-  ( ( A  e.  z  /\  A. y  e.  z  ( y  +  1 )  e.  z )  -> 
( A  +  1 )  e.  z )
1612, 15sylan2 286 . . . . 5  |-  ( ( A  e.  z  /\  z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } )  ->  ( A  + 
1 )  e.  z )
1716expcom 116 . . . 4  |-  ( z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }  ->  ( A  e.  z  ->  ( A  +  1 )  e.  z ) )
1817ralimia 2538 . . 3  |-  ( A. z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } A  e.  z  ->  A. z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }  ( A  +  1 )  e.  z )
195, 18syl 14 . 2  |-  ( A  e.  NN  ->  A. z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }  ( A  +  1 )  e.  z )
20 nnre 8924 . . . 4  |-  ( A  e.  NN  ->  A  e.  RR )
21 1red 7971 . . . 4  |-  ( A  e.  NN  ->  1  e.  RR )
2220, 21readdcld 7985 . . 3  |-  ( A  e.  NN  ->  ( A  +  1 )  e.  RR )
231eleq2i 2244 . . . 4  |-  ( ( A  +  1 )  e.  NN  <->  ( A  +  1 )  e. 
|^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) } )
24 elintg 3852 . . . 4  |-  ( ( A  +  1 )  e.  RR  ->  (
( A  +  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 ) }  ( A  +  1 )  e.  z ) )
2523, 24bitrid 192 . . 3  |-  ( ( A  +  1 )  e.  RR  ->  (
( A  +  1 )  e.  NN  <->  A. z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }  ( A  +  1 )  e.  z ) )
2622, 25syl 14 . 2  |-  ( A  e.  NN  ->  (
( A  +  1 )  e.  NN  <->  A. z  e.  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }  ( A  +  1 )  e.  z ) )
2719, 26mpbird 167 1  |-  ( A  e.  NN  ->  ( A  +  1 )  e.  NN )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    = wceq 1353    e. wcel 2148   {cab 2163   A.wral 2455   |^|cint 3844  (class class class)co 5874   RRcr 7809   1c1 7811    + caddc 7813   NNcn 8917
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4121  ax-cnex 7901  ax-resscn 7902  ax-1re 7904  ax-addrcl 7907
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877  df-inn 8918
This theorem is referenced by:  peano2nnd  8932  nnind  8933  nnaddcl  8937  2nn  9078  3nn  9079  4nn  9080  5nn  9081  6nn  9082  7nn  9083  8nn  9084  9nn  9085  nneoor  9353  10nn  9397  nnsplit  10134  fzonn0p1p1  10210  expp1  10524  facp1  10705  resqrexlemfp1  11013  resqrexlemcalc3  11020  trireciplem  11503  trirecip  11504  cvgratnnlemnexp  11527  cvgratz  11535  nno  11905  nnoddm1d2  11909  rplpwr  12022  prmind2  12114  sqrt2irr  12156  pcmpt  12335  pockthi  12350  mulgnnp1  12945  2sqlem10  14354
  Copyright terms: Public domain W3C validator