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

Theorem peano2 4591
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 2748 . 2  |-  ( A  e.  om  ->  A  e.  _V )
2 simpl 109 . . . . . 6  |-  ( ( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )  ->  A  e.  _V )
3 eleq1 2240 . . . . . . . 8  |-  ( x  =  A  ->  (
x  e.  z  <->  A  e.  z ) )
4 suceq 4399 . . . . . . . . 9  |-  ( x  =  A  ->  suc  x  =  suc  A )
54eleq1d 2246 . . . . . . . 8  |-  ( x  =  A  ->  ( suc  x  e.  z  <->  suc  A  e.  z ) )
63, 5imbi12d 234 . . . . . . 7  |-  ( x  =  A  ->  (
( x  e.  z  ->  suc  x  e.  z )  <->  ( A  e.  z  ->  suc  A  e.  z ) ) )
76adantl 277 . . . . . 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 2164 . . . . . . . . 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 110 . . . . . . . . . . . 12  |-  ( (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  A. x  e.  y  suc  x  e.  y )
10 df-ral 2460 . . . . . . . . . . . 12  |-  ( A. x  e.  y  suc  x  e.  y  <->  A. x
( x  e.  y  ->  suc  x  e.  y ) )
119, 10sylib 122 . . . . . . . . . . 11  |-  ( (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  A. x ( x  e.  y  ->  suc  x  e.  y )
)
1211sbimi 1764 . . . . . . . . . 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 1953 . . . . . . . . . . . 12  |-  ( [ z  /  y ] ( x  e.  y  ->  suc  x  e.  y )  <->  ( [
z  /  y ] x  e.  y  ->  [ z  /  y ] suc  x  e.  y ) )
14 clelsb2 2283 . . . . . . . . . . . . 13  |-  ( [ z  /  y ] x  e.  y  <->  x  e.  z )
15 clelsb2 2283 . . . . . . . . . . . . 13  |-  ( [ z  /  y ] suc  x  e.  y  <->  suc  x  e.  z )
1614, 15imbi12i 239 . . . . . . . . . . . 12  |-  ( ( [ z  /  y ] x  e.  y  ->  [ z  /  y ] suc  x  e.  y )  <->  ( x  e.  z  ->  suc  x  e.  z ) )
1713, 16bitri 184 . . . . . . . . . . 11  |-  ( [ z  /  y ] ( x  e.  y  ->  suc  x  e.  y )  <->  ( x  e.  z  ->  suc  x  e.  z ) )
1817sbalv 2005 . . . . . . . . . 10  |-  ( [ z  /  y ] A. x ( x  e.  y  ->  suc  x  e.  y )  <->  A. x ( x  e.  z  ->  suc  x  e.  z ) )
1912, 18sylib 122 . . . . . . . . 9  |-  ( [ z  /  y ] ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )  ->  A. x
( x  e.  z  ->  suc  x  e.  z ) )
208, 19sylbi 121 . . . . . . . 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 1558 . . . . . . 7  |-  ( z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  ->  (
x  e.  z  ->  suc  x  e.  z ) )
2221adantl 277 . . . . . 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 1528 . . . . . . 7  |-  F/ x  A  e.  _V
24 nfv 1528 . . . . . . . . 9  |-  F/ x (/) 
e.  y
25 nfra1 2508 . . . . . . . . 9  |-  F/ x A. x  e.  y  suc  x  e.  y
2624, 25nfan 1565 . . . . . . . 8  |-  F/ x
( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )
2726nfsab 2169 . . . . . . 7  |-  F/ x  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }
2823, 27nfan 1565 . . . . . 6  |-  F/ x
( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )
29 nfcvd 2320 . . . . . 6  |-  ( ( A  e.  _V  /\  z  e.  { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )  ->  F/_ x A )
30 nfvd 1529 . . . . . 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 2788 . . . . 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 2550 . . . 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 2536 . . . . 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 3850 . . . . . 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 4494 . . . . . . 7  |-  ( A  e.  _V  ->  suc  A  e.  _V )
36 elintg 3850 . . . . . . 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 234 . . . . 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 156 . . . 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 4588 . . . 4  |-  om  =  |^| { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }
4241eleq2i 2244 . . 3  |-  ( A  e.  om  <->  A  e.  |^|
{ y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )
4341eleq2i 2244 . . 3  |-  ( suc 
A  e.  om  <->  suc  A  e. 
|^| { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) } )
4440, 42, 433imtr4g 205 . 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 104    <-> wb 105   A.wal 1351    = wceq 1353   [wsb 1762    e. wcel 2148   {cab 2163   A.wral 2455   _Vcvv 2737   (/)c0 3422   |^|cint 3842   suc csuc 4362   omcom 4586
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-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430
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-pw 3576  df-sn 3597  df-pr 3598  df-uni 3808  df-int 3843  df-suc 4368  df-iom 4587
This theorem is referenced by:  peano5  4594  limom  4610  peano2b  4611  nnregexmid  4617  omsinds  4618  freccllem  6397  frecfcllem  6399  frecsuclem  6401  frecrdg  6403  nnacl  6475  nnacom  6479  nnmsucr  6483  nnsucsssuc  6487  nnaword  6506  1onn  6515  2onn  6516  3onn  6517  4onn  6518  nnaordex  6523  php5  6852  phplem4dom  6856  php5dom  6857  phplem4on  6861  dif1en  6873  findcard  6882  findcard2  6883  findcard2s  6884  infnfi  6889  unsnfi  6912  omp1eomlem  7087  ctmlemr  7101  infnninf  7116  infnninfOLD  7117  nnnninf  7118  nnnninfeq  7120  nninfwlpoimlemg  7167  nninfwlpoimlemginf  7168  frec2uzrand  10391  frecuzrdgsuc  10400  frecuzrdgsuctlem  10409  frecfzennn  10412  hashunlem  10768  ennnfonelemk  12384  ennnfonelemg  12387  ennnfonelemkh  12396  ennnfonelemhf1o  12397  ennnfonelemex  12398  ennnfonelemrn  12403  ennnfonelemnn0  12406  ctinfomlemom  12411  0nninf  14409  nnsf  14410  peano4nninf  14411  nninfsellemdc  14415  nninfsellemsuc  14417  nninfself  14418  nninfsellemeqinf  14421
  Copyright terms: Public domain W3C validator