Metamath Proof Explorer


Theorem fnlimfvre

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 fnlimfvre.p 𝑚 𝜑
fnlimfvre.m 𝑚 𝐹
fnlimfvre.n 𝑥 𝐹
fnlimfvre.z 𝑍 = ( ℤ𝑀 )
fnlimfvre.f ( ( 𝜑𝑚𝑍 ) → ( 𝐹𝑚 ) : dom ( 𝐹𝑚 ) ⟶ ℝ )
fnlimfvre.d 𝐷 = { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
fnlimfvre.x ( 𝜑𝑋𝐷 )
Assertion fnlimfvre ( 𝜑 → ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 fnlimfvre.p 𝑚 𝜑
2 fnlimfvre.m 𝑚 𝐹
3 fnlimfvre.n 𝑥 𝐹
4 fnlimfvre.z 𝑍 = ( ℤ𝑀 )
5 fnlimfvre.f ( ( 𝜑𝑚𝑍 ) → ( 𝐹𝑚 ) : dom ( 𝐹𝑚 ) ⟶ ℝ )
6 fnlimfvre.d 𝐷 = { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
7 fnlimfvre.x ( 𝜑𝑋𝐷 )
8 nfcv 𝑥 𝑍
9 nfcv 𝑥 ( ℤ𝑛 )
10 nfcv 𝑥 𝑚
11 3 10 nffv 𝑥 ( 𝐹𝑚 )
12 11 nfdm 𝑥 dom ( 𝐹𝑚 )
13 9 12 nfiin 𝑥 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 )
14 8 13 nfiun 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 )
15 14 ssrab2f { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ⊆ 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 )
16 6 15 eqsstri 𝐷 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 )
17 16 sseli ( 𝑋𝐷𝑋 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) )
18 eliun ( 𝑋 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ↔ ∃ 𝑛𝑍 𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) )
19 17 18 sylib ( 𝑋𝐷 → ∃ 𝑛𝑍 𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) )
20 7 19 syl ( 𝜑 → ∃ 𝑛𝑍 𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) )
21 nfv 𝑛 𝜑
22 nfv 𝑛 ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ
23 nfv 𝑚 𝑛𝑍
24 nfcv 𝑚 𝑋
25 nfii1 𝑚 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 )
26 24 25 nfel 𝑚 𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 )
27 1 23 26 nf3an 𝑚 ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) )
28 uzssz ( ℤ𝑀 ) ⊆ ℤ
29 4 eleq2i ( 𝑛𝑍𝑛 ∈ ( ℤ𝑀 ) )
30 29 biimpi ( 𝑛𝑍𝑛 ∈ ( ℤ𝑀 ) )
31 28 30 sseldi ( 𝑛𝑍𝑛 ∈ ℤ )
32 31 3ad2ant2 ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) → 𝑛 ∈ ℤ )
33 eqid ( ℤ𝑛 ) = ( ℤ𝑛 )
34 4 fvexi 𝑍 ∈ V
35 34 a1i ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) → 𝑍 ∈ V )
36 4 uztrn2 ( ( 𝑛𝑍𝑗 ∈ ( ℤ𝑛 ) ) → 𝑗𝑍 )
37 36 ssd ( 𝑛𝑍 → ( ℤ𝑛 ) ⊆ 𝑍 )
38 37 3ad2ant2 ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) → ( ℤ𝑛 ) ⊆ 𝑍 )
39 fvexd ( ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) ∧ 𝑚𝑍 ) → ( ( 𝐹𝑚 ) ‘ 𝑋 ) ∈ V )
40 fvexd ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) → ( ℤ𝑛 ) ∈ V )
41 ssidd ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) → ( ℤ𝑛 ) ⊆ ( ℤ𝑛 ) )
42 fvexd ( ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → ( ( 𝐹𝑚 ) ‘ 𝑋 ) ∈ V )
43 eqidd ( ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → ( ( 𝐹𝑚 ) ‘ 𝑋 ) = ( ( 𝐹𝑚 ) ‘ 𝑋 ) )
44 27 32 33 35 38 39 40 41 42 43 climfveqmpt ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) → ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) )
45 6 eleq2i ( 𝑋𝐷𝑋 ∈ { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )
46 45 biimpi ( 𝑋𝐷𝑋 ∈ { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } )
47 nfcv 𝑥 𝑋
48 11 47 nffv 𝑥 ( ( 𝐹𝑚 ) ‘ 𝑋 )
49 8 48 nfmpt 𝑥 ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) )
50 nfcv 𝑥 dom ⇝
51 49 50 nfel 𝑥 ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝
52 fveq2 ( 𝑥 = 𝑋 → ( ( 𝐹𝑚 ) ‘ 𝑥 ) = ( ( 𝐹𝑚 ) ‘ 𝑋 ) )
53 52 mpteq2dv ( 𝑥 = 𝑋 → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) )
54 53 eleq1d ( 𝑥 = 𝑋 → ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ ) )
55 47 14 51 54 elrabf ( 𝑋 ∈ { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ↔ ( 𝑋 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∧ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ ) )
56 55 biimpi ( 𝑋 ∈ { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } → ( 𝑋 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∧ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ ) )
57 56 simprd ( 𝑋 ∈ { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ )
58 46 57 syl ( 𝑋𝐷 → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ )
59 58 adantr ( ( 𝑋𝐷𝑛𝑍 ) → ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ )
60 nfmpt1 𝑚 ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) )
61 nfcv 𝑚 dom ⇝
62 60 61 nfel 𝑚 ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝
63 nfv 𝑚 𝑗𝑍
64 63 nfci 𝑚 𝑍
65 64 25 nfiun 𝑚 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 )
66 62 65 nfrabw 𝑚 { 𝑥 𝑛𝑍 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∣ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
67 6 66 nfcxfr 𝑚 𝐷
68 24 67 nfel 𝑚 𝑋𝐷
69 68 23 nfan 𝑚 ( 𝑋𝐷𝑛𝑍 )
70 31 adantl ( ( 𝑋𝐷𝑛𝑍 ) → 𝑛 ∈ ℤ )
71 34 a1i ( ( 𝑋𝐷𝑛𝑍 ) → 𝑍 ∈ V )
72 37 adantl ( ( 𝑋𝐷𝑛𝑍 ) → ( ℤ𝑛 ) ⊆ 𝑍 )
73 fvexd ( ( ( 𝑋𝐷𝑛𝑍 ) ∧ 𝑚𝑍 ) → ( ( 𝐹𝑚 ) ‘ 𝑋 ) ∈ V )
74 fvexd ( ( 𝑋𝐷𝑛𝑍 ) → ( ℤ𝑛 ) ∈ V )
75 ssidd ( ( 𝑋𝐷𝑛𝑍 ) → ( ℤ𝑛 ) ⊆ ( ℤ𝑛 ) )
76 fvexd ( ( ( 𝑋𝐷𝑛𝑍 ) ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → ( ( 𝐹𝑚 ) ‘ 𝑋 ) ∈ V )
77 eqidd ( ( ( 𝑋𝐷𝑛𝑍 ) ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → ( ( 𝐹𝑚 ) ‘ 𝑋 ) = ( ( 𝐹𝑚 ) ‘ 𝑋 ) )
78 69 70 33 71 72 73 74 75 76 77 climeldmeqmpt ( ( 𝑋𝐷𝑛𝑍 ) → ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ ) )
79 59 78 mpbid ( ( 𝑋𝐷𝑛𝑍 ) → ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ )
80 climdm ( ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) )
81 79 80 sylib ( ( 𝑋𝐷𝑛𝑍 ) → ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) )
82 7 81 sylan ( ( 𝜑𝑛𝑍 ) → ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) )
83 82 3adant3 ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) → ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) )
84 simpl1 ( ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → 𝜑 )
85 simpl2 ( ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → 𝑛𝑍 )
86 nfcv 𝑗 dom ( 𝐹𝑚 )
87 nfcv 𝑚 𝑗
88 2 87 nffv 𝑚 ( 𝐹𝑗 )
89 88 nfdm 𝑚 dom ( 𝐹𝑗 )
90 fveq2 ( 𝑚 = 𝑗 → ( 𝐹𝑚 ) = ( 𝐹𝑗 ) )
91 90 dmeqd ( 𝑚 = 𝑗 → dom ( 𝐹𝑚 ) = dom ( 𝐹𝑗 ) )
92 86 89 91 cbviin 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) = 𝑗 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑗 )
93 92 eleq2i ( 𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ↔ 𝑋 𝑗 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑗 ) )
94 93 biimpi ( 𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) → 𝑋 𝑗 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑗 ) )
95 94 adantr ( ( 𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → 𝑋 𝑗 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑗 ) )
96 simpr ( ( 𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → 𝑗 ∈ ( ℤ𝑛 ) )
97 eliinid ( ( 𝑋 𝑗 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑗 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → 𝑋 ∈ dom ( 𝐹𝑗 ) )
98 95 96 97 syl2anc ( ( 𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → 𝑋 ∈ dom ( 𝐹𝑗 ) )
99 98 3ad2antl3 ( ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → 𝑋 ∈ dom ( 𝐹𝑗 ) )
100 simpr ( ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → 𝑗 ∈ ( ℤ𝑛 ) )
101 id ( 𝑗 ∈ ( ℤ𝑛 ) → 𝑗 ∈ ( ℤ𝑛 ) )
102 fvexd ( 𝑗 ∈ ( ℤ𝑛 ) → ( ( 𝐹𝑗 ) ‘ 𝑋 ) ∈ V )
103 88 24 nffv 𝑚 ( ( 𝐹𝑗 ) ‘ 𝑋 )
104 90 fveq1d ( 𝑚 = 𝑗 → ( ( 𝐹𝑚 ) ‘ 𝑋 ) = ( ( 𝐹𝑗 ) ‘ 𝑋 ) )
105 eqid ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) )
106 87 103 104 105 fvmptf ( ( 𝑗 ∈ ( ℤ𝑛 ) ∧ ( ( 𝐹𝑗 ) ‘ 𝑋 ) ∈ V ) → ( ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ‘ 𝑗 ) = ( ( 𝐹𝑗 ) ‘ 𝑋 ) )
107 101 102 106 syl2anc ( 𝑗 ∈ ( ℤ𝑛 ) → ( ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ‘ 𝑗 ) = ( ( 𝐹𝑗 ) ‘ 𝑋 ) )
108 107 adantl ( ( ( 𝜑𝑛𝑍𝑋 ∈ dom ( 𝐹𝑗 ) ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → ( ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ‘ 𝑗 ) = ( ( 𝐹𝑗 ) ‘ 𝑋 ) )
109 simpll ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → 𝜑 )
110 36 adantll ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → 𝑗𝑍 )
111 1 63 nfan 𝑚 ( 𝜑𝑗𝑍 )
112 nfcv 𝑚
113 88 89 112 nff 𝑚 ( 𝐹𝑗 ) : dom ( 𝐹𝑗 ) ⟶ ℝ
114 111 113 nfim 𝑚 ( ( 𝜑𝑗𝑍 ) → ( 𝐹𝑗 ) : dom ( 𝐹𝑗 ) ⟶ ℝ )
115 eleq1w ( 𝑚 = 𝑗 → ( 𝑚𝑍𝑗𝑍 ) )
116 115 anbi2d ( 𝑚 = 𝑗 → ( ( 𝜑𝑚𝑍 ) ↔ ( 𝜑𝑗𝑍 ) ) )
117 90 91 feq12d ( 𝑚 = 𝑗 → ( ( 𝐹𝑚 ) : dom ( 𝐹𝑚 ) ⟶ ℝ ↔ ( 𝐹𝑗 ) : dom ( 𝐹𝑗 ) ⟶ ℝ ) )
118 116 117 imbi12d ( 𝑚 = 𝑗 → ( ( ( 𝜑𝑚𝑍 ) → ( 𝐹𝑚 ) : dom ( 𝐹𝑚 ) ⟶ ℝ ) ↔ ( ( 𝜑𝑗𝑍 ) → ( 𝐹𝑗 ) : dom ( 𝐹𝑗 ) ⟶ ℝ ) ) )
119 114 118 5 chvarfv ( ( 𝜑𝑗𝑍 ) → ( 𝐹𝑗 ) : dom ( 𝐹𝑗 ) ⟶ ℝ )
120 109 110 119 syl2anc ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑗 ) : dom ( 𝐹𝑗 ) ⟶ ℝ )
121 120 3adantl3 ( ( ( 𝜑𝑛𝑍𝑋 ∈ dom ( 𝐹𝑗 ) ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑗 ) : dom ( 𝐹𝑗 ) ⟶ ℝ )
122 simpl3 ( ( ( 𝜑𝑛𝑍𝑋 ∈ dom ( 𝐹𝑗 ) ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → 𝑋 ∈ dom ( 𝐹𝑗 ) )
123 121 122 ffvelrnd ( ( ( 𝜑𝑛𝑍𝑋 ∈ dom ( 𝐹𝑗 ) ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → ( ( 𝐹𝑗 ) ‘ 𝑋 ) ∈ ℝ )
124 108 123 eqeltrd ( ( ( 𝜑𝑛𝑍𝑋 ∈ dom ( 𝐹𝑗 ) ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → ( ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ‘ 𝑗 ) ∈ ℝ )
125 84 85 99 100 124 syl31anc ( ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → ( ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ‘ 𝑗 ) ∈ ℝ )
126 33 32 83 125 climrecl ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) → ( ⇝ ‘ ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )
127 44 126 eqeltrd ( ( 𝜑𝑛𝑍𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) ) → ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )
128 127 3exp ( 𝜑 → ( 𝑛𝑍 → ( 𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) → ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ ) ) )
129 21 22 128 rexlimd ( 𝜑 → ( ∃ 𝑛𝑍 𝑋 𝑚 ∈ ( ℤ𝑛 ) dom ( 𝐹𝑚 ) → ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ ) )
130 20 129 mpd ( 𝜑 → ( ⇝ ‘ ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )