MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ulmcau Structured version   Visualization version   GIF version

Theorem ulmcau 24440
Description: A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < 𝑥 there is a 𝑗 such that for all 𝑗𝑘 the functions 𝐹(𝑘) and 𝐹(𝑗) are uniformly within 𝑥 of each other on 𝑆. This is the four-quantifier version, see ulmcau2 24441 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.)
Hypotheses
Ref Expression
ulmcau.z 𝑍 = (ℤ𝑀)
ulmcau.m (𝜑𝑀 ∈ ℤ)
ulmcau.s (𝜑𝑆𝑉)
ulmcau.f (𝜑𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
Assertion
Ref Expression
ulmcau (𝜑 → (𝐹 ∈ dom (⇝𝑢𝑆) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
Distinct variable groups:   𝑗,𝑘,𝑥,𝑧,𝐹   𝜑,𝑗,𝑘,𝑥,𝑧   𝑆,𝑗,𝑘,𝑥,𝑧   𝑗,𝑍,𝑘,𝑥,𝑧   𝑗,𝑀,𝑘,𝑧
Allowed substitution hints:   𝑀(𝑥)   𝑉(𝑥,𝑧,𝑗,𝑘)

Proof of Theorem ulmcau
Dummy variables 𝑔 𝑚 𝑛 𝑝 𝑞 𝑟 𝑣 𝑤 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldmg 5487 . . . 4 (𝐹 ∈ dom (⇝𝑢𝑆) → (𝐹 ∈ dom (⇝𝑢𝑆) ↔ ∃𝑔 𝐹(⇝𝑢𝑆)𝑔))
21ibi 258 . . 3 (𝐹 ∈ dom (⇝𝑢𝑆) → ∃𝑔 𝐹(⇝𝑢𝑆)𝑔)
3 ulmcau.z . . . . . . . 8 𝑍 = (ℤ𝑀)
4 ulmcau.m . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
54ad2antrr 717 . . . . . . . 8 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈ ℤ)
6 ulmcau.f . . . . . . . . 9 (𝜑𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
76ad2antrr 717 . . . . . . . 8 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
8 eqidd 2766 . . . . . . . 8 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ (𝑘𝑍𝑧𝑆)) → ((𝐹𝑘)‘𝑧) = ((𝐹𝑘)‘𝑧))
9 eqidd 2766 . . . . . . . 8 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑧𝑆) → (𝑔𝑧) = (𝑔𝑧))
10 simplr 785 . . . . . . . 8 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → 𝐹(⇝𝑢𝑆)𝑔)
11 rphalfcl 12056 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ+)
1211adantl 473 . . . . . . . 8 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
133, 5, 7, 8, 9, 10, 12ulmi 24431 . . . . . . 7 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2))
14 simpr 477 . . . . . . . . . . 11 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗𝑍)
1514, 3syl6eleq 2854 . . . . . . . . . 10 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗 ∈ (ℤ𝑀))
16 eluzelz 11896 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℤ)
17 uzid 11901 . . . . . . . . . 10 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
18 fveq2 6375 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
1918fveq1d 6377 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝐹𝑘)‘𝑧) = ((𝐹𝑗)‘𝑧))
2019fvoveq1d 6864 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) = (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))))
2120breq1d 4819 . . . . . . . . . . . 12 (𝑘 = 𝑗 → ((abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ↔ (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
2221ralbidv 3133 . . . . . . . . . . 11 (𝑘 = 𝑗 → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
2322rspcv 3457 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑗) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
2415, 16, 17, 234syl 19 . . . . . . . . 9 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
25 r19.26 3211 . . . . . . . . . . . . . . 15 (∀𝑧𝑆 ((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) ↔ (∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
267ffvelrnda 6549 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (𝐹𝑗) ∈ (ℂ ↑𝑚 𝑆))
2726adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑗) ∈ (ℂ ↑𝑚 𝑆))
28 elmapi 8082 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑗) ∈ (ℂ ↑𝑚 𝑆) → (𝐹𝑗):𝑆⟶ℂ)
2927, 28syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑗):𝑆⟶ℂ)
3029ffvelrnda 6549 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((𝐹𝑗)‘𝑧) ∈ ℂ)
31 ulmcl 24426 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹(⇝𝑢𝑆)𝑔𝑔:𝑆⟶ℂ)
3231ad4antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑔:𝑆⟶ℂ)
3332ffvelrnda 6549 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (𝑔𝑧) ∈ ℂ)
3430, 33abssubd 14479 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) = (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))))
3534breq1d 4819 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ↔ (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
3635biimpd 220 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
373uztrn2 11904 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
38 ffvelrn 6547 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹:𝑍⟶(ℂ ↑𝑚 𝑆) ∧ 𝑘𝑍) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
397, 37, 38syl2an 589 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
4039anassrs 459 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
41 elmapi 8082 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆) → (𝐹𝑘):𝑆⟶ℂ)
4240, 41syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘):𝑆⟶ℂ)
4342ffvelrnda 6549 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
44 rpre 12036 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
4544ad4antlr 726 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → 𝑥 ∈ ℝ)
46 abs3lem 14365 . . . . . . . . . . . . . . . . . . 19 (((((𝐹𝑘)‘𝑧) ∈ ℂ ∧ ((𝐹𝑗)‘𝑧) ∈ ℂ) ∧ ((𝑔𝑧) ∈ ℂ ∧ 𝑥 ∈ ℝ)) → (((abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
4743, 30, 33, 45, 46syl22anc 867 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (((abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
4836, 47sylan2d 598 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (((abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
4948ancomsd 457 . . . . . . . . . . . . . . . 16 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5049ralimdva 3109 . . . . . . . . . . . . . . 15 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑧𝑆 ((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5125, 50syl5bir 234 . . . . . . . . . . . . . 14 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5251expdimp 444 . . . . . . . . . . . . 13 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5352an32s 642 . . . . . . . . . . . 12 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5453ralimdva 3109 . . . . . . . . . . 11 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5554ex 401 . . . . . . . . . 10 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥)))
5655com23 86 . . . . . . . . 9 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → (∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥)))
5724, 56mpdd 43 . . . . . . . 8 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5857reximdva 3163 . . . . . . 7 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5913, 58mpd 15 . . . . . 6 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥)
6059ralrimiva 3113 . . . . 5 ((𝜑𝐹(⇝𝑢𝑆)𝑔) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥)
6160ex 401 . . . 4 (𝜑 → (𝐹(⇝𝑢𝑆)𝑔 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
6261exlimdv 2028 . . 3 (𝜑 → (∃𝑔 𝐹(⇝𝑢𝑆)𝑔 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
632, 62syl5 34 . 2 (𝜑 → (𝐹 ∈ dom (⇝𝑢𝑆) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
64 ulmrel 24423 . . . 4 Rel (⇝𝑢𝑆)
65 ulmcau.s . . . . . . . . . 10 (𝜑𝑆𝑉)
663, 4, 65, 6ulmcaulem 24439 . . . . . . . . 9 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
6766biimpa 468 . . . . . . . 8 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥)
68 rphalfcl 12056 . . . . . . . 8 (𝑟 ∈ ℝ+ → (𝑟 / 2) ∈ ℝ+)
69 breq2 4813 . . . . . . . . . . . . 13 (𝑥 = (𝑟 / 2) → ((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
7069ralbidv 3133 . . . . . . . . . . . 12 (𝑥 = (𝑟 / 2) → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
71702ralbidv 3136 . . . . . . . . . . 11 (𝑥 = (𝑟 / 2) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
7271rexbidv 3199 . . . . . . . . . 10 (𝑥 = (𝑟 / 2) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
73 ralcom 3245 . . . . . . . . . . . . . 14 (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑚 ∈ (ℤ𝑞)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2))
74 fveq2 6375 . . . . . . . . . . . . . . 15 (𝑞 = 𝑘 → (ℤ𝑞) = (ℤ𝑘))
75 fveq2 6375 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑧 → ((𝐹𝑞)‘𝑤) = ((𝐹𝑞)‘𝑧))
76 fveq2 6375 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑧 → ((𝐹𝑚)‘𝑤) = ((𝐹𝑚)‘𝑧))
7775, 76oveq12d 6860 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑧 → (((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤)) = (((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧)))
7877fveq2d 6379 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑧 → (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) = (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))))
7978breq1d 4819 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑧 → ((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8079cbvralv 3319 . . . . . . . . . . . . . . . 16 (∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2))
81 fveq2 6375 . . . . . . . . . . . . . . . . . . . 20 (𝑞 = 𝑘 → (𝐹𝑞) = (𝐹𝑘))
8281fveq1d 6377 . . . . . . . . . . . . . . . . . . 19 (𝑞 = 𝑘 → ((𝐹𝑞)‘𝑧) = ((𝐹𝑘)‘𝑧))
8382fvoveq1d 6864 . . . . . . . . . . . . . . . . . 18 (𝑞 = 𝑘 → (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) = (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))))
8483breq1d 4819 . . . . . . . . . . . . . . . . 17 (𝑞 = 𝑘 → ((abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2) ↔ (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8584ralbidv 3133 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑘 → (∀𝑧𝑆 (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2) ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8680, 85syl5bb 274 . . . . . . . . . . . . . . 15 (𝑞 = 𝑘 → (∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8774, 86raleqbidv 3300 . . . . . . . . . . . . . 14 (𝑞 = 𝑘 → (∀𝑚 ∈ (ℤ𝑞)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8873, 87syl5bb 274 . . . . . . . . . . . . 13 (𝑞 = 𝑘 → (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8988cbvralv 3319 . . . . . . . . . . . 12 (∀𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑘 ∈ (ℤ𝑝)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2))
90 fveq2 6375 . . . . . . . . . . . . 13 (𝑝 = 𝑗 → (ℤ𝑝) = (ℤ𝑗))
9190raleqdv 3292 . . . . . . . . . . . 12 (𝑝 = 𝑗 → (∀𝑘 ∈ (ℤ𝑝)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
9289, 91syl5bb 274 . . . . . . . . . . 11 (𝑝 = 𝑗 → (∀𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
9392cbvrexv 3320 . . . . . . . . . 10 (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2))
9472, 93syl6bbr 280 . . . . . . . . 9 (𝑥 = (𝑟 / 2) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2)))
9594rspccva 3460 . . . . . . . 8 ((∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ∧ (𝑟 / 2) ∈ ℝ+) → ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2))
9667, 68, 95syl2an 589 . . . . . . 7 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2))
973uztrn2 11904 . . . . . . . . . . 11 ((𝑝𝑍𝑞 ∈ (ℤ𝑝)) → 𝑞𝑍)
98 eqid 2765 . . . . . . . . . . . . . 14 (ℤ𝑞) = (ℤ𝑞)
99 eluzelz 11896 . . . . . . . . . . . . . . . 16 (𝑞 ∈ (ℤ𝑀) → 𝑞 ∈ ℤ)
10099, 3eleq2s 2862 . . . . . . . . . . . . . . 15 (𝑞𝑍𝑞 ∈ ℤ)
101100ad2antlr 718 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → 𝑞 ∈ ℤ)
10268adantl 473 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈ ℝ+)
103102ad2antrr 717 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (𝑟 / 2) ∈ ℝ+)
104 simplr 785 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → 𝑞𝑍)
1053uztrn2 11904 . . . . . . . . . . . . . . . 16 ((𝑞𝑍𝑚 ∈ (ℤ𝑞)) → 𝑚𝑍)
106104, 105sylan 575 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → 𝑚𝑍)
107 fveq2 6375 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → (𝐹𝑛) = (𝐹𝑚))
108107fveq1d 6377 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → ((𝐹𝑛)‘𝑤) = ((𝐹𝑚)‘𝑤))
109 eqid 2765 . . . . . . . . . . . . . . . 16 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) = (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))
110 fvex 6388 . . . . . . . . . . . . . . . 16 ((𝐹𝑚)‘𝑤) ∈ V
111108, 109, 110fvmpt 6471 . . . . . . . . . . . . . . 15 (𝑚𝑍 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))‘𝑚) = ((𝐹𝑚)‘𝑤))
112106, 111syl 17 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))‘𝑚) = ((𝐹𝑚)‘𝑤))
1136adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
114113ffvelrnda 6549 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑛𝑍) → (𝐹𝑛) ∈ (ℂ ↑𝑚 𝑆))
115 elmapi 8082 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑛) ∈ (ℂ ↑𝑚 𝑆) → (𝐹𝑛):𝑆⟶ℂ)
116114, 115syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑛𝑍) → (𝐹𝑛):𝑆⟶ℂ)
117116ffvelrnda 6549 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑛𝑍) ∧ 𝑦𝑆) → ((𝐹𝑛)‘𝑦) ∈ ℂ)
118117an32s 642 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑦) ∈ ℂ)
119118fmpttd 6575 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)):𝑍⟶ℂ)
120119ffvelrnda 6549 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) ∧ 𝑞𝑍) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) ∈ ℂ)
121 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑦 → ((𝐹𝑘)‘𝑧) = ((𝐹𝑘)‘𝑦))
122 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑦 → ((𝐹𝑗)‘𝑧) = ((𝐹𝑗)‘𝑦))
123121, 122oveq12d 6860 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑦 → (((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧)) = (((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦)))
124123fveq2d 6379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑦 → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) = (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))))
125124breq1d 4819 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑦 → ((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
126125rspcv 3457 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝑆 → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 → (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
127126ralimdv 3110 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝑆 → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 → ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
128127reximdv 3162 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝑆 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
129128ralimdv 3110 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝑆 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
130129impcom 396 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥𝑦𝑆) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥)
131130adantll 705 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥)
132 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑞 = 𝑘 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) = ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘))
133132fvoveq1d 6864 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑞 = 𝑘 → (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) = (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))))
134133breq1d 4819 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑞 = 𝑘 → ((abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟))
135134cbvralv 3319 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟)
136 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 = 𝑗 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝) = ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))
137136oveq2d 6858 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 = 𝑗 → (((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝)) = (((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗)))
138137fveq2d 6379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑝 = 𝑗 → (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) = (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))))
139138breq1d 4819 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 = 𝑗 → ((abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟))
14090, 139raleqbidv 3300 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = 𝑗 → (∀𝑘 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟))
141135, 140syl5bb 274 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑗 → (∀𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟))
142141cbvrexv 3320 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟)
143 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
144143fveq1d 6377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑘 → ((𝐹𝑛)‘𝑦) = ((𝐹𝑘)‘𝑦))
145 eqid 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) = (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))
146 fvex 6388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹𝑘)‘𝑦) ∈ V
147144, 145, 146fvmpt 6471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘𝑍 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) = ((𝐹𝑘)‘𝑦))
14837, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) = ((𝐹𝑘)‘𝑦))
149 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑗 → (𝐹𝑛) = (𝐹𝑗))
150149fveq1d 6377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑗 → ((𝐹𝑛)‘𝑦) = ((𝐹𝑗)‘𝑦))
151 fvex 6388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹𝑗)‘𝑦) ∈ V
152150, 145, 151fvmpt 6471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗𝑍 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗) = ((𝐹𝑗)‘𝑦))
153152adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗) = ((𝐹𝑗)‘𝑦))
154148, 153oveq12d 6860 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → (((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗)) = (((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦)))
155154fveq2d 6379 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) = (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))))
156155breq1d 4819 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → ((abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟 ↔ (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟))
157156ralbidva 3132 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗𝑍 → (∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟))
158157rexbiia 3187 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟)
159142, 158bitri 266 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟)
160 breq2 4813 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑟 = 𝑥 → ((abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟 ↔ (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
161160ralbidv 3133 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 = 𝑥 → (∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
162161rexbidv 3199 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 = 𝑥 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
163159, 162syl5bb 274 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = 𝑥 → (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
164163cbvralv 3319 . . . . . . . . . . . . . . . . . . . 20 (∀𝑟 ∈ ℝ+𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥)
165131, 164sylibr 225 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → ∀𝑟 ∈ ℝ+𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟)
1663fvexi 6389 . . . . . . . . . . . . . . . . . . . . 21 𝑍 ∈ V
167166mptex 6679 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ V
168167a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ V)
1693, 120, 165, 168caucvg 14696 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ )
170169ralrimiva 3113 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → ∀𝑦𝑆 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ )
171170ad2antrr 717 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) → ∀𝑦𝑆 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ )
172 fveq2 6375 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑤 → ((𝐹𝑛)‘𝑦) = ((𝐹𝑛)‘𝑤))
173172mpteq2dv 4904 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑤 → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) = (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)))
174173eleq1d 2829 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑤 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ ↔ (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ∈ dom ⇝ ))
175174rspccva 3460 . . . . . . . . . . . . . . . 16 ((∀𝑦𝑆 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ ∧ 𝑤𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ∈ dom ⇝ )
176171, 175sylan 575 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ∈ dom ⇝ )
177 climdm 14572 . . . . . . . . . . . . . . 15 ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ∈ dom ⇝ ↔ (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
178176, 177sylib 209 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
17998, 101, 103, 112, 178climi2 14529 . . . . . . . . . . . . 13 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)(abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2))
18098r19.29uz 14377 . . . . . . . . . . . . . . 15 ((∀𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)(abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)))
18198r19.2uz 14378 . . . . . . . . . . . . . . 15 (∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → ∃𝑚 ∈ (ℤ𝑞)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)))
182180, 181syl 17 . . . . . . . . . . . . . 14 ((∀𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)(abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → ∃𝑚 ∈ (ℤ𝑞)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)))
1836ad2antrr 717 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
184183ffvelrnda 6549 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) → (𝐹𝑞) ∈ (ℂ ↑𝑚 𝑆))
185 elmapi 8082 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑞) ∈ (ℂ ↑𝑚 𝑆) → (𝐹𝑞):𝑆⟶ℂ)
186184, 185syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) → (𝐹𝑞):𝑆⟶ℂ)
187186ffvelrnda 6549 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → ((𝐹𝑞)‘𝑤) ∈ ℂ)
188187adantr 472 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → ((𝐹𝑞)‘𝑤) ∈ ℂ)
189 climcl 14517 . . . . . . . . . . . . . . . . . 18 ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ ℂ)
190178, 189syl 17 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ ℂ)
191190adantr 472 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ ℂ)
1926ad5antr 728 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
193192, 106ffvelrnd 6550 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → (𝐹𝑚) ∈ (ℂ ↑𝑚 𝑆))
194 elmapi 8082 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑚) ∈ (ℂ ↑𝑚 𝑆) → (𝐹𝑚):𝑆⟶ℂ)
195193, 194syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → (𝐹𝑚):𝑆⟶ℂ)
196 simplr 785 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → 𝑤𝑆)
197195, 196ffvelrnd 6550 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → ((𝐹𝑚)‘𝑤) ∈ ℂ)
198 rpre 12036 . . . . . . . . . . . . . . . . 17 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
199198ad4antlr 726 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → 𝑟 ∈ ℝ)
200 abs3lem 14365 . . . . . . . . . . . . . . . 16 (((((𝐹𝑞)‘𝑤) ∈ ℂ ∧ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ ℂ) ∧ (((𝐹𝑚)‘𝑤) ∈ ℂ ∧ 𝑟 ∈ ℝ)) → (((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
201188, 191, 197, 199, 200syl22anc 867 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → (((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
202201rexlimdva 3178 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (∃𝑚 ∈ (ℤ𝑞)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
203182, 202syl5 34 . . . . . . . . . . . . 13 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → ((∀𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)(abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
204179, 203mpan2d 685 . . . . . . . . . . . 12 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (∀𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
205204ralimdva 3109 . . . . . . . . . . 11 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) → (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
20697, 205sylan2 586 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ (𝑝𝑍𝑞 ∈ (ℤ𝑝))) → (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
207206anassrs 459 . . . . . . . . 9 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑝𝑍) ∧ 𝑞 ∈ (ℤ𝑝)) → (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
208207ralimdva 3109 . . . . . . . 8 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑝𝑍) → (∀𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
209208reximdva 3163 . . . . . . 7 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
21096, 209mpd 15 . . . . . 6 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟)
211210ralrimiva 3113 . . . . 5 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → ∀𝑟 ∈ ℝ+𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟)
2124adantr 472 . . . . . 6 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝑀 ∈ ℤ)
213 eqidd 2766 . . . . . 6 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ (𝑞𝑍𝑤𝑆)) → ((𝐹𝑞)‘𝑤) = ((𝐹𝑞)‘𝑤))
214173fveq2d 6379 . . . . . . . 8 (𝑦 = 𝑤 → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))) = ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
215 eqid 2765 . . . . . . . 8 (𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)))) = (𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))
216 fvex 6388 . . . . . . . 8 ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ V
217214, 215, 216fvmpt 6471 . . . . . . 7 (𝑤𝑆 → ((𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))‘𝑤) = ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
218217adantl 473 . . . . . 6 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑤𝑆) → ((𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))‘𝑤) = ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
219 climdm 14572 . . . . . . . . 9 ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ ↔ (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))
220169, 219sylib 209 . . . . . . . 8 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))
221 climcl 14517 . . . . . . . 8 ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))) ∈ ℂ)
222220, 221syl 17 . . . . . . 7 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))) ∈ ℂ)
223222fmpttd 6575 . . . . . 6 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → (𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)))):𝑆⟶ℂ)
22465adantr 472 . . . . . 6 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝑆𝑉)
2253, 212, 113, 213, 218, 223, 224ulm2 24430 . . . . 5 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → (𝐹(⇝𝑢𝑆)(𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)))) ↔ ∀𝑟 ∈ ℝ+𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
226211, 225mpbird 248 . . . 4 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝐹(⇝𝑢𝑆)(𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)))))
227 releldm 5527 . . . 4 ((Rel (⇝𝑢𝑆) ∧ 𝐹(⇝𝑢𝑆)(𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))) → 𝐹 ∈ dom (⇝𝑢𝑆))
22864, 226, 227sylancr 581 . . 3 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝐹 ∈ dom (⇝𝑢𝑆))
229228ex 401 . 2 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥𝐹 ∈ dom (⇝𝑢𝑆)))
23063, 229impbid 203 1 (𝜑 → (𝐹 ∈ dom (⇝𝑢𝑆) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wex 1874  wcel 2155  wral 3055  wrex 3056  Vcvv 3350   class class class wbr 4809  cmpt 4888  dom cdm 5277  Rel wrel 5282  wf 6064  cfv 6068  (class class class)co 6842  𝑚 cmap 8060  cc 10187  cr 10188   < clt 10328  cmin 10520   / cdiv 10938  2c2 11327  cz 11624  cuz 11886  +crp 12028  abscabs 14261  cli 14502  𝑢culm 24421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-map 8062  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-sup 8555  df-inf 8556  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-ico 12383  df-fl 12801  df-seq 13009  df-exp 13068  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-limsup 14489  df-clim 14506  df-rlim 14507  df-ulm 24422
This theorem is referenced by:  ulmcau2  24441  mtest  24449
  Copyright terms: Public domain W3C validator