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

Theorem peano2 4346
Description: The successor of any natural number is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.)
Assertion
Ref Expression
peano2  |-  ( A  e.  om  ->  suc  A  e.  om )

Proof of Theorem peano2
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2583 . 2  |-  ( A  e.  om  ->  A  e.  _V )
2 simpl 106 . . . . . 6  |-  ( ( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )  ->  A  e.  _V )
3 eleq1 2116 . . . . . . . 8  |-  ( x  =  A  ->  (
x  e.  z  <->  A  e.  z ) )
4 suceq 4167 . . . . . . . . 9  |-  ( x  =  A  ->  suc  x  =  suc  A )
54eleq1d 2122 . . . . . . . 8  |-  ( x  =  A  ->  ( suc  x  e.  z  <->  suc  A  e.  z ) )
63, 5imbi12d 227 . . . . . . 7  |-  ( x  =  A  ->  (
( x  e.  z  ->  suc  x  e.  z )  <->  ( A  e.  z  ->  suc  A  e.  z ) ) )
76adantl 266 . . . . . 6  |-  ( ( ( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )  /\  x  =  A )  ->  ( (
x  e.  z  ->  suc  x  e.  z )  <-> 
( A  e.  z  ->  suc  A  e.  z ) ) )
8 df-clab 2043 . . . . . . . . 9  |-  ( 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 ) )
9 simpr 107 . . . . . . . . . . . 12  |-  ( (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  A. x  e.  y  suc  x  e.  y )
10 df-ral 2328 . . . . . . . . . . . 12  |-  ( A. x  e.  y  suc  x  e.  y  <->  A. x
( x  e.  y  ->  suc  x  e.  y ) )
119, 10sylib 131 . . . . . . . . . . 11  |-  ( (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  A. x ( x  e.  y  ->  suc  x  e.  y )
)
1211sbimi 1663 . . . . . . . . . 10  |-  ( [ z  /  y ] ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  [ z  /  y ] A. x ( x  e.  y  ->  suc  x  e.  y ) )
13 sbim 1843 . . . . . . . . . . . 12  |-  ( [ z  /  y ] ( x  e.  y  ->  suc  x  e.  y )  <->  ( [
z  /  y ] x  e.  y  ->  [ z  /  y ] suc  x  e.  y ) )
14 elsb4 1869 . . . . . . . . . . . . 13  |-  ( [ z  /  y ] x  e.  y  <->  x  e.  z )
15 clelsb4 2159 . . . . . . . . . . . . 13  |-  ( [ z  /  y ] suc  x  e.  y  <->  suc  x  e.  z )
1614, 15imbi12i 232 . . . . . . . . . . . 12  |-  ( ( [ z  /  y ] x  e.  y  ->  [ z  /  y ] suc  x  e.  y )  <->  ( x  e.  z  ->  suc  x  e.  z ) )
1713, 16bitri 177 . . . . . . . . . . 11  |-  ( [ z  /  y ] ( x  e.  y  ->  suc  x  e.  y )  <->  ( x  e.  z  ->  suc  x  e.  z ) )
1817sbalv 1897 . . . . . . . . . 10  |-  ( [ z  /  y ] A. x ( x  e.  y  ->  suc  x  e.  y )  <->  A. x ( x  e.  z  ->  suc  x  e.  z ) )
1912, 18sylib 131 . . . . . . . . 9  |-  ( [ z  /  y ] ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  A. x
( x  e.  z  ->  suc  x  e.  z ) )
208, 19sylbi 118 . . . . . . . 8  |-  ( z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ->  A. x
( x  e.  z  ->  suc  x  e.  z ) )
212019.21bi 1466 . . . . . . 7  |-  ( z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ->  (
x  e.  z  ->  suc  x  e.  z ) )
2221adantl 266 . . . . . 6  |-  ( ( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )  ->  ( x  e.  z  ->  suc  x  e.  z ) )
23 nfv 1437 . . . . . . 7  |-  F/ x  A  e.  _V
24 nfv 1437 . . . . . . . . 9  |-  F/ x (/) 
e.  y
25 nfra1 2372 . . . . . . . . 9  |-  F/ x A. x  e.  y  suc  x  e.  y
2624, 25nfan 1473 . . . . . . . 8  |-  F/ x
( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )
2726nfsab 2048 . . . . . . 7  |-  F/ x  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }
2823, 27nfan 1473 . . . . . 6  |-  F/ x
( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )
29 nfcvd 2195 . . . . . 6  |-  ( ( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )  ->  F/_ x A )
30 nfvd 1438 . . . . . 6  |-  ( ( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )  ->  F/ x ( A  e.  z  ->  suc  A  e.  z ) )
312, 7, 22, 28, 29, 30vtocldf 2622 . . . . 5  |-  ( ( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )  ->  ( A  e.  z  ->  suc  A  e.  z ) )
3231ralrimiva 2409 . . . 4  |-  ( A  e.  _V  ->  A. z  e.  { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ( A  e.  z  ->  suc  A  e.  z ) )
33 ralim 2397 . . . . 5  |-  ( A. z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ( A  e.  z  ->  suc 
A  e.  z )  ->  ( A. z  e.  { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } A  e.  z  ->  A. z  e.  {
y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } suc  A  e.  z ) )
34 elintg 3651 . . . . . 6  |-  ( A  e.  _V  ->  ( A  e.  |^| { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  <->  A. z  e.  { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } A  e.  z ) )
35 sucexg 4252 . . . . . . 7  |-  ( A  e.  _V  ->  suc  A  e.  _V )
36 elintg 3651 . . . . . . 7  |-  ( suc 
A  e.  _V  ->  ( suc  A  e.  |^| { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  <->  A. z  e.  { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } suc  A  e.  z ) )
3735, 36syl 14 . . . . . 6  |-  ( A  e.  _V  ->  ( suc  A  e.  |^| { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  <->  A. z  e.  { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } suc  A  e.  z ) )
3834, 37imbi12d 227 . . . . 5  |-  ( A  e.  _V  ->  (
( A  e.  |^| { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ->  suc 
A  e.  |^| { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )  <-> 
( A. z  e. 
{ y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } A  e.  z  ->  A. z  e.  {
y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } suc  A  e.  z ) ) )
3933, 38syl5ibr 149 . . . 4  |-  ( A  e.  _V  ->  ( A. z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ( A  e.  z  ->  suc 
A  e.  z )  ->  ( A  e. 
|^| { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ->  suc  A  e. 
|^| { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } ) ) )
4032, 39mpd 13 . . 3  |-  ( A  e.  _V  ->  ( A  e.  |^| { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ->  suc 
A  e.  |^| { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } ) )
41 dfom3 4343 . . . 4  |-  om  =  |^| { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }
4241eleq2i 2120 . . 3  |-  ( A  e.  om  <->  A  e.  |^|
{ y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )
4341eleq2i 2120 . . 3  |-  ( suc 
A  e.  om  <->  suc  A  e. 
|^| { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )
4440, 42, 433imtr4g 198 . 2  |-  ( A  e.  _V  ->  ( A  e.  om  ->  suc 
A  e.  om )
)
451, 44mpcom 36 1  |-  ( A  e.  om  ->  suc  A  e.  om )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102   A.wal 1257    = wceq 1259    e. wcel 1409   [wsb 1661   {cab 2042   A.wral 2323   _Vcvv 2574   (/)c0 3252   |^|cint 3643   suc csuc 4130   omcom 4341
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3903  ax-pow 3955  ax-pr 3972  ax-un 4198
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-v 2576  df-un 2950  df-in 2952  df-ss 2959  df-pw 3389  df-sn 3409  df-pr 3410  df-uni 3609  df-int 3644  df-suc 4136  df-iom 4342
This theorem is referenced by:  peano5  4349  limom  4364  peano2b  4365  nnregexmid  4370  frecsuclem1  6018  frecsuclem3  6021  frecrdg  6023  nnacl  6090  nnacom  6094  nnmsucr  6098  nnsucsssuc  6102  nnaword  6115  1onn  6124  2onn  6125  3onn  6126  4onn  6127  nnaordex  6131  php5  6352  phplem4dom  6355  php5dom  6356  phplem4on  6360  dif1en  6368  findcard  6376  findcard2  6377  findcard2s  6378  frec2uzrand  9355  frecuzrdgsuc  9365  frecfzennn  9367
  Copyright terms: Public domain W3C validator