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 ⊢ Ⅎ _ x D
fnlimfv.2 ⊢ Ⅎ _ x F
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 ⊢ Ⅎ _ x D
2 fnlimfv.2 ⊢ Ⅎ _ x F
3 fnlimfv.3 ⊢ G = x ∈ D ⟼ ⇝ ⁡ m ∈ Z ⟼ F ⁡ m ⁡ x
4 fnlimfv.4 ⊢ φ → X ∈ D
5 nfcv ⊢ Ⅎ _ y D
6 nfcv ⊢ Ⅎ _ y ⇝ ⁡ m ∈ Z ⟼ F ⁡ m ⁡ x
7 nfcv ⊢ Ⅎ _ x ⇝
8 nfcv ⊢ Ⅎ _ x Z
9 nfcv ⊢ Ⅎ _ x m
10 2 9 nffv ⊢ Ⅎ _ x F ⁡ m
11 nfcv ⊢ Ⅎ _ x y
12 10 11 nffv ⊢ Ⅎ _ x F ⁡ m ⁡ y
13 8 12 nfmpt ⊢ Ⅎ _ x m ∈ 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