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