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 ( 𝜑 → ( 𝐺𝑋 ) = ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) )