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

Theorem iseqvalcbv 9583
Description: Changing the bound variables in an expression which appears in some  seq related proofs. (Contributed by Jim Kingdon, 28-Apr-2022.)
Assertion
Ref Expression
iseqvalcbv  |- frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  T  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) ,  <. M ,  ( F `  M )
>. )  = frec (
( a  e.  (
ZZ>= `  M ) ,  b  e.  T  |->  <.
( a  +  1 ) ,  ( a ( c  e.  (
ZZ>= `  M ) ,  d  e.  S  |->  ( d  .+  ( F `
 ( c  +  1 ) ) ) ) b ) >.
) ,  <. M , 
( F `  M
) >. )
Distinct variable groups:    .+ , a, b, c, d, x, y   
w,  .+ , z, c,
d    F, a, b, c, d, x, y    w, F, z    M, a, b, c, d, x, y   
w, M, z    S, a, b, c, d, x, y    w, S, z    T, a, b, x, y
Allowed substitution hints:    T( z, w, c, d)

Proof of Theorem iseqvalcbv
StepHypRef Expression
1 oveq1 5570 . . . . . . . . . 10  |-  ( c  =  z  ->  (
c  +  1 )  =  ( z  +  1 ) )
21fveq2d 5233 . . . . . . . . 9  |-  ( c  =  z  ->  ( F `  ( c  +  1 ) )  =  ( F `  ( z  +  1 ) ) )
32oveq2d 5579 . . . . . . . 8  |-  ( c  =  z  ->  (
d  .+  ( F `  ( c  +  1 ) ) )  =  ( d  .+  ( F `  ( z  +  1 ) ) ) )
4 oveq1 5570 . . . . . . . 8  |-  ( d  =  w  ->  (
d  .+  ( F `  ( z  +  1 ) ) )  =  ( w  .+  ( F `  ( z  +  1 ) ) ) )
53, 4cbvmpt2v 5635 . . . . . . 7  |-  ( c  e.  ( ZZ>= `  M
) ,  d  e.  S  |->  ( d  .+  ( F `  ( c  +  1 ) ) ) )  =  ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) )
65oveqi 5576 . . . . . 6  |-  ( x ( c  e.  (
ZZ>= `  M ) ,  d  e.  S  |->  ( d  .+  ( F `
 ( c  +  1 ) ) ) ) y )  =  ( x ( z  e.  ( ZZ>= `  M
) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
76opeq2i 3594 . . . . 5  |-  <. (
x  +  1 ) ,  ( x ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d 
.+  ( F `  ( c  +  1 ) ) ) ) y ) >.  =  <. ( x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >.
87a1i 9 . . . 4  |-  ( ( x  e.  ( ZZ>= `  M )  /\  y  e.  T )  ->  <. (
x  +  1 ) ,  ( x ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d 
.+  ( F `  ( c  +  1 ) ) ) ) y ) >.  =  <. ( x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. )
98mpt2eq3ia 5621 . . 3  |-  ( x  e.  ( ZZ>= `  M
) ,  y  e.  T  |->  <. ( x  + 
1 ) ,  ( x ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d  .+  ( F `  ( c  +  1 ) ) ) ) y )
>. )  =  (
x  e.  ( ZZ>= `  M ) ,  y  e.  T  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. )
10 oveq1 5570 . . . . 5  |-  ( x  =  a  ->  (
x  +  1 )  =  ( a  +  1 ) )
11 oveq1 5570 . . . . 5  |-  ( x  =  a  ->  (
x ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d  .+  ( F `  ( c  +  1 ) ) ) ) y )  =  ( a ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d 
.+  ( F `  ( c  +  1 ) ) ) ) y ) )
1210, 11opeq12d 3598 . . . 4  |-  ( x  =  a  ->  <. (
x  +  1 ) ,  ( x ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d 
.+  ( F `  ( c  +  1 ) ) ) ) y ) >.  =  <. ( a  +  1 ) ,  ( a ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d 
.+  ( F `  ( c  +  1 ) ) ) ) y ) >. )
13 oveq2 5571 . . . . 5  |-  ( y  =  b  ->  (
a ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d  .+  ( F `  ( c  +  1 ) ) ) ) y )  =  ( a ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d 
.+  ( F `  ( c  +  1 ) ) ) ) b ) )
1413opeq2d 3597 . . . 4  |-  ( y  =  b  ->  <. (
a  +  1 ) ,  ( a ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d 
.+  ( F `  ( c  +  1 ) ) ) ) y ) >.  =  <. ( a  +  1 ) ,  ( a ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d 
.+  ( F `  ( c  +  1 ) ) ) ) b ) >. )
1512, 14cbvmpt2v 5635 . . 3  |-  ( x  e.  ( ZZ>= `  M
) ,  y  e.  T  |->  <. ( x  + 
1 ) ,  ( x ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d  .+  ( F `  ( c  +  1 ) ) ) ) y )
>. )  =  (
a  e.  ( ZZ>= `  M ) ,  b  e.  T  |->  <. (
a  +  1 ) ,  ( a ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d 
.+  ( F `  ( c  +  1 ) ) ) ) b ) >. )
169, 15eqtr3i 2105 . 2  |-  ( x  e.  ( ZZ>= `  M
) ,  y  e.  T  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. )  =  (
a  e.  ( ZZ>= `  M ) ,  b  e.  T  |->  <. (
a  +  1 ) ,  ( a ( c  e.  ( ZZ>= `  M ) ,  d  e.  S  |->  ( d 
.+  ( F `  ( c  +  1 ) ) ) ) b ) >. )
17 freceq1 6061 . 2  |-  ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  T  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. )  =  ( a  e.  ( ZZ>= `  M ) ,  b  e.  T  |-> 
<. ( a  +  1 ) ,  ( a ( c  e.  (
ZZ>= `  M ) ,  d  e.  S  |->  ( d  .+  ( F `
 ( c  +  1 ) ) ) ) b ) >.
)  -> frec ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  T  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) ,  <. M ,  ( F `  M )
>. )  = frec (
( a  e.  (
ZZ>= `  M ) ,  b  e.  T  |->  <.
( a  +  1 ) ,  ( a ( c  e.  (
ZZ>= `  M ) ,  d  e.  S  |->  ( d  .+  ( F `
 ( c  +  1 ) ) ) ) b ) >.
) ,  <. M , 
( F `  M
) >. ) )
1816, 17ax-mp 7 1  |- frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  T  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) ,  <. M ,  ( F `  M )
>. )  = frec (
( a  e.  (
ZZ>= `  M ) ,  b  e.  T  |->  <.
( a  +  1 ) ,  ( a ( c  e.  (
ZZ>= `  M ) ,  d  e.  S  |->  ( d  .+  ( F `
 ( c  +  1 ) ) ) ) b ) >.
) ,  <. M , 
( F `  M
) >. )
Colors of variables: wff set class
Syntax hints:    /\ wa 102    = wceq 1285    e. wcel 1434   <.cop 3419   ` cfv 4952  (class class class)co 5563    |-> cmpt2 5565  freccfrec 6059   1c1 7096    + caddc 7098   ZZ>=cuz 8752
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-pow 3968  ax-pr 3992
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2612  df-un 2986  df-in 2988  df-ss 2995  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-br 3806  df-opab 3860  df-mpt 3861  df-res 4403  df-iota 4917  df-fv 4960  df-ov 5566  df-oprab 5567  df-mpt2 5568  df-recs 5974  df-frec 6060
This theorem is referenced by:  iseq1t  9586  iseqfclt  9588  iseqp1t  9591
  Copyright terms: Public domain W3C validator