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 ⊢Ⅎ_xD
fnlimfv.2 ⊢Ⅎ_xF
fnlimfv.3 ⊢G=x∈D⟼⇝⁡m∈Z⟼F⁡m⁡x
fnlimfv.4 ⊢φ→X∈D
Assertion fnlimfv ⊢φ→G⁡X=⇝⁡m∈Z⟼F⁡m⁡X

Proof

Step Hyp Ref Expression
1 fnlimfv.1 ⊢Ⅎ_xD
2 fnlimfv.2 ⊢Ⅎ_xF
3 fnlimfv.3 ⊢G=x∈D⟼⇝⁡m∈Z⟼F⁡m⁡x
4 fnlimfv.4 ⊢φ→X∈D
5 nfcv ⊢Ⅎ_yD
6 nfcv ⊢Ⅎ_y⇝⁡m∈Z⟼F⁡m⁡x
7 nfcv ⊢Ⅎ_x⇝
8 nfcv ⊢Ⅎ_xZ
9 nfcv ⊢Ⅎ_xm
10 2 9 nffv ⊢Ⅎ_xF⁡m
11 nfcv ⊢Ⅎ_xy
12 10 11 nffv ⊢Ⅎ_xF⁡m⁡y
13 8 12 nfmpt ⊢Ⅎ_xm∈Z⟼F⁡m⁡y
14 7 13 nffv ⊢Ⅎ_x⇝⁡m∈Z⟼F⁡m⁡y
15 fveq2 ⊢x=y→F⁡m⁡x=F⁡m⁡y
16 15 mpteq2dv ⊢x=y→m∈Z⟼F⁡m⁡x=m∈Z⟼F⁡m⁡y
17 16 fveq2d ⊢x=y→⇝⁡m∈Z⟼F⁡m⁡x=⇝⁡m∈Z⟼F⁡m⁡y
18 1 5 6 14 17 cbvmptf ⊢x∈D⟼⇝⁡m∈Z⟼F⁡m⁡x=y∈D⟼⇝⁡m∈Z⟼F⁡m⁡y
19 3 18 eqtri ⊢G=y∈D⟼⇝⁡m∈Z⟼F⁡m⁡y
20 fveq2 ⊢y=X→F⁡m⁡y=F⁡m⁡X
21 20 mpteq2dv ⊢y=X→m∈Z⟼F⁡m⁡y=m∈Z⟼F⁡m⁡X
22 21 fveq2d ⊢y=X→⇝⁡m∈Z⟼F⁡m⁡y=⇝⁡m∈Z⟼F⁡m⁡X
23 fvexd ⊢φ→⇝⁡m∈Z⟼F⁡m⁡X∈V
24 19 22 4 23 fvmptd3 ⊢φ→G⁡X=⇝⁡m∈Z⟼F⁡m⁡X