Metamath Proof Explorer


Theorem fnlimfvre2

Description: The limit function of real functions, applied to elements in its domain, evaluates to Real values. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses fnlimfvre2.p 𝑚 𝜑
fnlimfvre2.m 𝑚 𝐹
fnlimfvre2.n 𝑥 𝐹
fnlimfvre2.z 𝑍 = ( ℤ𝑀 )
fnlimfvre2.f ( ( 𝜑𝑚𝑍 ) → ( 𝐹𝑚 ) : dom ( 𝐹𝑚 ) ⟶ ℝ )
fnlimfvre2.d 𝐷 = { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
fnlimfvre2.g 𝐺 = ( 𝑥𝐷 ↦ ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ) )
fnlimfvre2.x ( 𝜑𝑋𝐷 )
Assertion fnlimfvre2 ( 𝜑 → ( 𝐺𝑋 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 fnlimfvre2.p 𝑚 𝜑
2 fnlimfvre2.m 𝑚 𝐹
3 fnlimfvre2.n 𝑥 𝐹
4 fnlimfvre2.z 𝑍 = ( ℤ𝑀 )
5 fnlimfvre2.f ( ( 𝜑𝑚𝑍 ) → ( 𝐹𝑚 ) : dom ( 𝐹𝑚 ) ⟶ ℝ )
6 fnlimfvre2.d 𝐷 = { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
7 fnlimfvre2.g 𝐺 = ( 𝑥𝐷 ↦ ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ) )
8 fnlimfvre2.x ( 𝜑𝑋𝐷 )
9 nfrab1 𝑥 { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
10 6 9 nfcxfr 𝑥 𝐷
11 nfcv 𝑧 𝐷
12 nfcv 𝑧 ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) )
13 nfcv 𝑥
14 nfcv 𝑥 𝑍
15 nfcv 𝑥 𝑚
16 3 15 nffv 𝑥 ( 𝐹𝑚 )
17 nfcv 𝑥 𝑧
18 16 17 nffv 𝑥 ( ( 𝐹𝑚 ) ‘ 𝑧 )
19 14 18 nfmpt 𝑥 ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) )
20 13 19 nffv 𝑥 ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) )
21 fveq2 ( 𝑥 = 𝑧 → ( ( 𝐹𝑚 ) ‘ 𝑥 ) = ( ( 𝐹𝑚 ) ‘ 𝑧 ) )
22 21 mpteq2dv ( 𝑥 = 𝑧 → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) )
23 22 fveq2d ( 𝑥 = 𝑧 → ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) ) )
24 10 11 12 20 23 cbvmptf ( 𝑥𝐷 ↦ ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑧𝐷 ↦ ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) ) )
25 7 24 eqtri 𝐺 = ( 𝑧𝐷 ↦ ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) ) )
26 fveq2 ( 𝑋 = 𝑧 → ( ( 𝐹𝑚 ) ‘ 𝑋 ) = ( ( 𝐹𝑚 ) ‘ 𝑧 ) )
27 26 mpteq2dv ( 𝑋 = 𝑧 → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) )
28 eqcom ( 𝑋 = 𝑧𝑧 = 𝑋 )
29 28 imbi1i ( ( 𝑋 = 𝑧 → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) ) ↔ ( 𝑧 = 𝑋 → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) ) )
30 eqcom ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) ↔ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) )
31 30 imbi2i ( ( 𝑧 = 𝑋 → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) ) ↔ ( 𝑧 = 𝑋 → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) )
32 29 31 bitri ( ( 𝑋 = 𝑧 → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) ) ↔ ( 𝑧 = 𝑋 → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) )
33 27 32 mpbi ( 𝑧 = 𝑋 → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) )
34 33 fveq2d ( 𝑧 = 𝑋 → ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑧 ) ) ) = ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) )
35 fvexd ( 𝜑 → ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) ∈ V )
36 25 34 8 35 fvmptd3 ( 𝜑 → ( 𝐺𝑋 ) = ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) )
37 1 2 3 4 5 6 8 fnlimfvre ( 𝜑 → ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )
38 36 37 eqeltrd ( 𝜑 → ( 𝐺𝑋 ) ∈ ℝ )