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