Metamath Proof Explorer

Theorem fnlimfv

Description: The value of the limit function G at any point of its domain D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses fnlimfv.1 
|- F/_ x D
fnlimfv.2 
|- F/_ x F
fnlimfv.3 
|- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
fnlimfv.4 
|- ( ph -> X e. D )
Assertion fnlimfv 
|- ( ph -> ( G ` X ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) )

Proof

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 ) ) ) )