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 sselid ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑋 ∈ 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 ⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )