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 ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )