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 ⊢ Ⅎ 𝑥 𝐷
fnlimfv.2 ⊢ Ⅎ 𝑥 𝐹
fnlimfv.3 ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
fnlimfv.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
Assertion fnlimfv ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 fnlimfv.1 ⊢ Ⅎ 𝑥 𝐷
2 fnlimfv.2 ⊢ Ⅎ 𝑥 𝐹
3 fnlimfv.3 ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
4 fnlimfv.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
5 nfcv ⊢ Ⅎ 𝑦 𝐷
6 nfcv ⊢ Ⅎ 𝑦 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
7 nfcv ⊢ Ⅎ 𝑥 ⇝
8 nfcv ⊢ Ⅎ 𝑥 𝑍
9 nfcv ⊢ Ⅎ 𝑥 𝑚
10 2 9 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑚 )
11 nfcv ⊢ Ⅎ 𝑥 𝑦
12 10 11 nffv ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 )
13 8 12 nfmpt ⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) )
14 7 13 nffv ⊢ Ⅎ 𝑥 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) )
15 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) )
16 15 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) )
17 16 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) )
18 1 5 6 14 17 cbvmptf ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) )
19 3 18 eqtri ⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) )
20 fveq2 ⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) )
21 20 mpteq2dv ⊢ ( 𝑦 = 𝑋 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) )
22 21 fveq2d ⊢ ( 𝑦 = 𝑋 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
23 fvexd ⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ V )
24 19 22 4 23 fvmptd3 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )