Step |
Hyp |
Ref |
Expression |
1 |
|
fnlimfv.1 |
|- F/_ x D |
2 |
|
fnlimfv.2 |
|- F/_ x F |
3 |
|
fnlimfv.3 |
|- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) |
4 |
|
fnlimfv.4 |
|- ( ph -> X e. D ) |
5 |
|
nfcv |
|- F/_ y D |
6 |
|
nfcv |
|- F/_ y ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) |
7 |
|
nfcv |
|- F/_ x ~~> |
8 |
|
nfcv |
|- F/_ x Z |
9 |
|
nfcv |
|- F/_ x m |
10 |
2 9
|
nffv |
|- F/_ x ( F ` m ) |
11 |
|
nfcv |
|- F/_ x y |
12 |
10 11
|
nffv |
|- F/_ x ( ( F ` m ) ` y ) |
13 |
8 12
|
nfmpt |
|- F/_ x ( m e. Z |-> ( ( F ` m ) ` y ) ) |
14 |
7 13
|
nffv |
|- F/_ x ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` y ) ) ) |
15 |
|
fveq2 |
|- ( x = y -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` y ) ) |
16 |
15
|
mpteq2dv |
|- ( x = y -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` y ) ) ) |
17 |
16
|
fveq2d |
|- ( x = y -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` y ) ) ) ) |
18 |
1 5 6 14 17
|
cbvmptf |
|- ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) = ( y e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` y ) ) ) ) |
19 |
3 18
|
eqtri |
|- G = ( y e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` y ) ) ) ) |
20 |
|
fveq2 |
|- ( y = X -> ( ( F ` m ) ` y ) = ( ( F ` m ) ` X ) ) |
21 |
20
|
mpteq2dv |
|- ( y = X -> ( m e. Z |-> ( ( F ` m ) ` y ) ) = ( m e. Z |-> ( ( F ` m ) ` X ) ) ) |
22 |
21
|
fveq2d |
|- ( y = X -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` y ) ) ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) ) |
23 |
|
fvexd |
|- ( ph -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. _V ) |
24 |
19 22 4 23
|
fvmptd3 |
|- ( ph -> ( G ` X ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) ) |