This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ulmcau

Description: A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < x there is a j such that for all j <_ k the functions F ( k ) and F ( j ) are uniformly within x of each other on S . This is the four-quantifier version, see ulmcau2 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypotheses ulmcau.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ulmcau.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ulmcau.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
ulmcau.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
Assertion ulmcau ( 𝜑 → ( 𝐹 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )

Proof

Step Hyp Ref Expression
1 ulmcau.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ulmcau.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 ulmcau.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4 ulmcau.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
5 eldmg ⊢ ( 𝐹 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) → ( 𝐹 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) ↔ ∃ 𝑔 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) )
6 5 ibi ⊢ ( 𝐹 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) → ∃ 𝑔 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 )
7 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
8 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
9 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
10 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑔 ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) )
11 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 )
12 rphalfcl ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) ∈ ℝ+ )
13 12 adantl ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) ∈ ℝ+ )
14 1 7 8 9 10 11 13 ulmi ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) )
15 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
16 15 1 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
17 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ )
18 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
19 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
20 19 fveq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) )
21 20 fvoveq1d ⊢ ( 𝑘 = 𝑗 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) )
22 21 breq1d ⊢ ( 𝑘 = 𝑗 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
23 22 ralbidv ⊢ ( 𝑘 = 𝑗 → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
24 23 rspcv ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
25 16 17 18 24 4syl ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
26 r19.26 ⊢ ( ∀ 𝑧 ∈ 𝑆 ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) ↔ ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
27 8 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ( ℂ ↑m 𝑆 ) )
28 27 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ( ℂ ↑m 𝑆 ) )
29 elmapi ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑗 ) : 𝑆 ⟶ ℂ )
30 28 29 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) : 𝑆 ⟶ ℂ )
31 30 ffvelcdmda ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ∈ ℂ )
32 ulmcl ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 → 𝑔 : 𝑆 ⟶ ℂ )
33 32 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑔 : 𝑆 ⟶ ℂ )
34 33 ffvelcdmda ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑔 ‘ 𝑧 ) ∈ ℂ )
35 31 34 abssubd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) = ( abs ‘ ( ( 𝑔 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) )
36 35 breq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ↔ ( abs ‘ ( ( 𝑔 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
37 36 biimpd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ( abs ‘ ( ( 𝑔 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
38 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
39 ffvelcdm ⊢ ( ( 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
40 8 38 39 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
41 40 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
42 elmapi ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
43 41 42 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
44 43 ffvelcdmda ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
45 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
46 45 ad4antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑥 ∈ ℝ )
47 abs3lem ⊢ ( ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ∈ ℂ ) ∧ ( ( 𝑔 ‘ 𝑧 ) ∈ ℂ ∧ 𝑥 ∈ ℝ ) ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ( abs ‘ ( ( 𝑔 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
48 44 31 34 46 47 syl22anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ( abs ‘ ( ( 𝑔 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
49 37 48 sylan2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
50 49 ancomsd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
51 50 ralimdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ∀ 𝑧 ∈ 𝑆 ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
52 26 51 biimtrrid ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
53 52 expdimp ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
54 53 an32s ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
55 54 ralimdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
56 55 ex ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ) )
57 56 com23 ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ) )
58 25 57 mpdd ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
59 58 reximdva ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑔 ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
60 14 59 mpd ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 )
61 60 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 )
62 61 ex ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
63 62 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑔 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝑔 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
64 6 63 syl5 ⊢ ( 𝜑 → ( 𝐹 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
65 ulmrel ⊢ Rel ( ⇝𝑢 ‘ 𝑆 )
66 1 2 3 4 ulmcaulem ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
67 66 biimpa ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 )
68 rphalfcl ⊢ ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) ∈ ℝ+ )
69 breq2 ⊢ ( 𝑥 = ( 𝑟 / 2 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
70 69 ralbidv ⊢ ( 𝑥 = ( 𝑟 / 2 ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
71 70 2ralbidv ⊢ ( 𝑥 = ( 𝑟 / 2 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
72 71 rexbidv ⊢ ( 𝑥 = ( 𝑟 / 2 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
73 ralcom ⊢ ( ∀ 𝑤 ∈ 𝑆 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) )
74 fveq2 ⊢ ( 𝑞 = 𝑘 → ( ℤ≥ ‘ 𝑞 ) = ( ℤ≥ ‘ 𝑘 ) )
75 fveq2 ⊢ ( 𝑤 = 𝑧 → ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑧 ) )
76 fveq2 ⊢ ( 𝑤 = 𝑧 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) )
77 75 76 oveq12d ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) = ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) )
78 77 fveq2d ⊢ ( 𝑤 = 𝑧 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) )
79 78 breq1d ⊢ ( 𝑤 = 𝑧 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
80 79 cbvralvw ⊢ ( ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) )
81 fveq2 ⊢ ( 𝑞 = 𝑘 → ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑘 ) )
82 81 fveq1d ⊢ ( 𝑞 = 𝑘 → ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
83 82 fvoveq1d ⊢ ( 𝑞 = 𝑘 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) )
84 83 breq1d ⊢ ( 𝑞 = 𝑘 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
85 84 ralbidv ⊢ ( 𝑞 = 𝑘 → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
86 80 85 bitrid ⊢ ( 𝑞 = 𝑘 → ( ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
87 74 86 raleqbidv ⊢ ( 𝑞 = 𝑘 → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
88 73 87 bitrid ⊢ ( 𝑞 = 𝑘 → ( ∀ 𝑤 ∈ 𝑆 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
89 88 cbvralvw ⊢ ( ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑤 ∈ 𝑆 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) )
90 fveq2 ⊢ ( 𝑝 = 𝑗 → ( ℤ≥ ‘ 𝑝 ) = ( ℤ≥ ‘ 𝑗 ) )
91 90 raleqdv ⊢ ( 𝑝 = 𝑗 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
92 89 91 bitrid ⊢ ( 𝑝 = 𝑗 → ( ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑤 ∈ 𝑆 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
93 92 cbvrexvw ⊢ ( ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑤 ∈ 𝑆 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) )
94 72 93 bitr4di ⊢ ( 𝑥 = ( 𝑟 / 2 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑤 ∈ 𝑆 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ) )
95 94 rspccva ⊢ ( ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ∧ ( 𝑟 / 2 ) ∈ ℝ+ ) → ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑤 ∈ 𝑆 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) )
96 67 68 95 syl2an ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑤 ∈ 𝑆 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) )
97 1 uztrn2 ⊢ ( ( 𝑝 ∈ 𝑍 ∧ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ) → 𝑞 ∈ 𝑍 )
98 eqid ⊢ ( ℤ≥ ‘ 𝑞 ) = ( ℤ≥ ‘ 𝑞 )
99 eluzelz ⊢ ( 𝑞 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑞 ∈ ℤ )
100 99 1 eleq2s ⊢ ( 𝑞 ∈ 𝑍 → 𝑞 ∈ ℤ )
101 100 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → 𝑞 ∈ ℤ )
102 68 adantl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑟 / 2 ) ∈ ℝ+ )
103 102 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝑟 / 2 ) ∈ ℝ+ )
104 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → 𝑞 ∈ 𝑍 )
105 1 uztrn2 ⊢ ( ( 𝑞 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ) → 𝑚 ∈ 𝑍 )
106 104 105 sylan ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ) → 𝑚 ∈ 𝑍 )
107 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) )
108 107 fveq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
109 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) )
110 fvex ⊢ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ∈ V
111 108 109 110 fvmpt ⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
112 106 111 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
113 4 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
114 113 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑆 ) )
115 elmapi ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑛 ) : 𝑆 ⟶ ℂ )
116 114 115 syl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : 𝑆 ⟶ ℂ )
117 116 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ∈ ℂ )
118 117 an32s ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ∈ ℂ )
119 118 fmpttd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) : 𝑍 ⟶ ℂ )
120 119 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑞 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑞 ) ∈ ℂ )
121 fveq2 ⊢ ( 𝑧 = 𝑦 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) )
122 fveq2 ⊢ ( 𝑧 = 𝑦 → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) )
123 121 122 oveq12d ⊢ ( 𝑧 = 𝑦 → ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) )
124 123 fveq2d ⊢ ( 𝑧 = 𝑦 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) )
125 124 breq1d ⊢ ( 𝑧 = 𝑦 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑥 ) )
126 125 rspcv ⊢ ( 𝑦 ∈ 𝑆 → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑥 ) )
127 126 ralimdv ⊢ ( 𝑦 ∈ 𝑆 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑥 ) )
128 127 reximdv ⊢ ( 𝑦 ∈ 𝑆 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑥 ) )
129 128 ralimdv ⊢ ( 𝑦 ∈ 𝑆 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑥 ) )
130 129 impcom ⊢ ( ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ∧ 𝑦 ∈ 𝑆 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑥 )
131 130 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑦 ∈ 𝑆 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑥 )
132 fveq2 ⊢ ( 𝑞 = 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑞 ) = ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) )
133 132 fvoveq1d ⊢ ( 𝑞 = 𝑘 → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑞 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) = ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) )
134 133 breq1d ⊢ ( 𝑞 = 𝑘 → ( ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑞 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) < 𝑟 ↔ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) < 𝑟 ) )
135 134 cbvralvw ⊢ ( ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑞 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) < 𝑟 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑝 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) < 𝑟 )
136 fveq2 ⊢ ( 𝑝 = 𝑗 → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) = ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) )
137 136 oveq2d ⊢ ( 𝑝 = 𝑗 → ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) = ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) )
138 137 fveq2d ⊢ ( 𝑝 = 𝑗 → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) = ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) )
139 138 breq1d ⊢ ( 𝑝 = 𝑗 → ( ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) < 𝑟 ↔ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) < 𝑟 ) )
140 90 139 raleqbidv ⊢ ( 𝑝 = 𝑗 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑝 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) < 𝑟 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) < 𝑟 ) )
141 135 140 bitrid ⊢ ( 𝑝 = 𝑗 → ( ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑞 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) < 𝑟 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) < 𝑟 ) )
142 141 cbvrexvw ⊢ ( ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑞 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) < 𝑟 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) < 𝑟 )
143 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
144 143 fveq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) )
145 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) )
146 fvex ⊢ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ∈ V
147 144 145 146 fvmpt ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) )
148 38 147 syl ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) )
149 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) )
150 149 fveq1d ⊢ ( 𝑛 = 𝑗 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) )
151 fvex ⊢ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ∈ V
152 150 145 151 fvmpt ⊢ ( 𝑗 ∈ 𝑍 → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) )
153 152 adantr ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) )
154 148 153 oveq12d ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) = ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) )
155 154 fveq2d ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) )
156 155 breq1d ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) < 𝑟 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑟 ) )
157 156 ralbidva ⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) < 𝑟 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑟 ) )
158 157 rexbiia ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) < 𝑟 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑟 )
159 142 158 bitri ⊢ ( ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑞 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) < 𝑟 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑟 )
160 breq2 ⊢ ( 𝑟 = 𝑥 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑟 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑥 ) )
161 160 ralbidv ⊢ ( 𝑟 = 𝑥 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑟 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑥 ) )
162 161 rexbidv ⊢ ( 𝑟 = 𝑥 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑟 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑥 ) )
163 159 162 bitrid ⊢ ( 𝑟 = 𝑥 → ( ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑞 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) < 𝑟 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑥 ) )
164 163 cbvralvw ⊢ ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑞 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) < 𝑟 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) < 𝑥 )
165 131 164 sylibr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑦 ∈ 𝑆 ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑞 ) − ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑝 ) ) ) < 𝑟 )
166 1 fvexi ⊢ 𝑍 ∈ V
167 166 mptex ⊢ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ∈ V
168 167 a1i ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ∈ V )
169 1 120 165 168 caucvg ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ∈ dom ⇝ )
170 169 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) → ∀ 𝑦 ∈ 𝑆 ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ∈ dom ⇝ )
171 170 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) → ∀ 𝑦 ∈ 𝑆 ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ∈ dom ⇝ )
172 fveq2 ⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) )
173 172 mpteq2dv ⊢ ( 𝑦 = 𝑤 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) )
174 173 eleq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ∈ dom ⇝ ↔ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ∈ dom ⇝ ) )
175 174 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑆 ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ∈ dom ⇝ ∧ 𝑤 ∈ 𝑆 ) → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ∈ dom ⇝ )
176 171 175 sylan ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ∈ dom ⇝ )
177 climdm ⊢ ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ∈ dom ⇝ ↔ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ⇝ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) )
178 176 177 sylib ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ⇝ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) )
179 98 101 103 112 178 climi2 ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ∃ 𝑣 ∈ ( ℤ≥ ‘ 𝑞 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑣 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < ( 𝑟 / 2 ) )
180 98 r19.29uz ⊢ ( ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ∧ ∃ 𝑣 ∈ ( ℤ≥ ‘ 𝑞 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑣 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < ( 𝑟 / 2 ) ) → ∃ 𝑣 ∈ ( ℤ≥ ‘ 𝑞 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑣 ) ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < ( 𝑟 / 2 ) ) )
181 98 r19.2uz ⊢ ( ∃ 𝑣 ∈ ( ℤ≥ ‘ 𝑞 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑣 ) ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < ( 𝑟 / 2 ) ) → ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < ( 𝑟 / 2 ) ) )
182 180 181 syl ⊢ ( ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ∧ ∃ 𝑣 ∈ ( ℤ≥ ‘ 𝑞 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑣 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < ( 𝑟 / 2 ) ) → ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < ( 𝑟 / 2 ) ) )
183 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
184 183 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑞 ) ∈ ( ℂ ↑m 𝑆 ) )
185 elmapi ⊢ ( ( 𝐹 ‘ 𝑞 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑞 ) : 𝑆 ⟶ ℂ )
186 184 185 syl ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑞 ) : 𝑆 ⟶ ℂ )
187 186 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ∈ ℂ )
188 187 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ) → ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ∈ ℂ )
189 climcl ⊢ ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ⇝ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) → ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ∈ ℂ )
190 178 189 syl ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ∈ ℂ )
191 190 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ) → ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ∈ ℂ )
192 4 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
193 192 106 ffvelcdmd ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ( ℂ ↑m 𝑆 ) )
194 elmapi ⊢ ( ( 𝐹 ‘ 𝑚 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑚 ) : 𝑆 ⟶ ℂ )
195 193 194 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ) → ( 𝐹 ‘ 𝑚 ) : 𝑆 ⟶ ℂ )
196 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ) → 𝑤 ∈ 𝑆 )
197 195 196 ffvelcdmd ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ∈ ℂ )
198 rpre ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
199 198 ad4antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ) → 𝑟 ∈ ℝ )
200 abs3lem ⊢ ( ( ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) ∈ ℂ ∧ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ∈ ℂ ) ∧ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ∈ ℂ ∧ 𝑟 ∈ ℝ ) ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < ( 𝑟 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < 𝑟 ) )
201 188 191 197 199 200 syl22anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < ( 𝑟 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < 𝑟 ) )
202 201 rexlimdva ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < ( 𝑟 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < 𝑟 ) )
203 182 202 syl5 ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) ∧ ∃ 𝑣 ∈ ( ℤ≥ ‘ 𝑞 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑣 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < ( 𝑟 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < 𝑟 ) )
204 179 203 mpan2d ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < 𝑟 ) )
205 204 ralimdva ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑞 ∈ 𝑍 ) → ( ∀ 𝑤 ∈ 𝑆 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) → ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < 𝑟 ) )
206 97 205 sylan2 ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑝 ∈ 𝑍 ∧ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ) ) → ( ∀ 𝑤 ∈ 𝑆 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) → ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < 𝑟 ) )
207 206 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑝 ∈ 𝑍 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ) → ( ∀ 𝑤 ∈ 𝑆 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) → ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < 𝑟 ) )
208 207 ralimdva ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑝 ∈ 𝑍 ) → ( ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑤 ∈ 𝑆 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) → ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < 𝑟 ) )
209 208 reximdva ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑤 ∈ 𝑆 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑞 ) ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) ) < ( 𝑟 / 2 ) → ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < 𝑟 ) )
210 96 209 mpd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < 𝑟 )
211 210 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < 𝑟 )
212 2 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) → 𝑀 ∈ ℤ )
213 eqidd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ ( 𝑞 ∈ 𝑍 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) )
214 173 fveq2d ⊢ ( 𝑦 = 𝑤 → ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) = ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) )
215 eqid ⊢ ( 𝑦 ∈ 𝑆 ↦ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝑆 ↦ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) )
216 fvex ⊢ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ∈ V
217 214 215 216 fvmpt ⊢ ( 𝑤 ∈ 𝑆 → ( ( 𝑦 ∈ 𝑆 ↦ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) ) ‘ 𝑤 ) = ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) )
218 217 adantl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝑦 ∈ 𝑆 ↦ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) ) ‘ 𝑤 ) = ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) )
219 climdm ⊢ ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ∈ dom ⇝ ↔ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ⇝ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) )
220 169 219 sylib ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ⇝ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) )
221 climcl ⊢ ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ⇝ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) → ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) ∈ ℂ )
222 220 221 syl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) ∧ 𝑦 ∈ 𝑆 ) → ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) ∈ ℂ )
223 222 fmpttd ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) → ( 𝑦 ∈ 𝑆 ↦ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) ) : 𝑆 ⟶ ℂ )
224 3 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) → 𝑆 ∈ 𝑉 )
225 1 212 113 213 218 223 224 ulm2 ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) ( 𝑦 ∈ 𝑆 ↦ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) ) ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑝 ∈ 𝑍 ∀ 𝑞 ∈ ( ℤ≥ ‘ 𝑝 ) ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑞 ) ‘ 𝑤 ) − ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) ) ) ) < 𝑟 ) )
226 211 225 mpbird ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) ( 𝑦 ∈ 𝑆 ↦ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) ) )
227 releldm ⊢ ( ( Rel ( ⇝𝑢 ‘ 𝑆 ) ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) ( 𝑦 ∈ 𝑆 ↦ ( ⇝ ‘ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) ) ) → 𝐹 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) )
228 65 226 227 sylancr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) → 𝐹 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) )
229 228 ex ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 → 𝐹 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) ) )
230 64 229 impbid ⊢ ( 𝜑 → ( 𝐹 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )