metucn

Description: Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn . (Contributed by Thierry Arnoux, 26-Jan-2018) (Revised by Thierry Arnoux, 11-Feb-2018)

	Ref	Expression
Hypotheses	metucn.u	⊢ 𝑈 = ( metUnif ‘ 𝐶 )
	metucn.v	⊢ 𝑉 = ( metUnif ‘ 𝐷 )
	metucn.x	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
	metucn.y	⊢ ( 𝜑 → 𝑌 ≠ ∅ )
	metucn.c	⊢ ( 𝜑 → 𝐶 ∈ ( PsMet ‘ 𝑋 ) )
	metucn.d	⊢ ( 𝜑 → 𝐷 ∈ ( PsMet ‘ 𝑌 ) )
Assertion	metucn	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑈 Cn_u 𝑉 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑑 ∈ ℝ⁺ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐶 𝑦 ) < 𝑐 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		metucn.u	⊢ 𝑈 = ( metUnif ‘ 𝐶 )
2		metucn.v	⊢ 𝑉 = ( metUnif ‘ 𝐷 )
3		metucn.x	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
4		metucn.y	⊢ ( 𝜑 → 𝑌 ≠ ∅ )
5		metucn.c	⊢ ( 𝜑 → 𝐶 ∈ ( PsMet ‘ 𝑋 ) )
6		metucn.d	⊢ ( 𝜑 → 𝐷 ∈ ( PsMet ‘ 𝑌 ) )
7		metuval	⊢ ( 𝐶 ∈ ( PsMet ‘ 𝑋 ) → ( metUnif ‘ 𝐶 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ) )
8	5 7	syl	⊢ ( 𝜑 → ( metUnif ‘ 𝐶 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ) )
9	1 8	eqtrid	⊢ ( 𝜑 → 𝑈 = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ) )
10		metuval	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑌 ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) )
11	6 10	syl	⊢ ( 𝜑 → ( metUnif ‘ 𝐷 ) = ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) )
12	2 11	eqtrid	⊢ ( 𝜑 → 𝑉 = ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) )
13	9 12	oveq12d	⊢ ( 𝜑 → ( 𝑈 Cn_u 𝑉 ) = ( ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ) Cn_u ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ) )
14	13	eleq2d	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑈 Cn_u 𝑉 ) ↔ 𝐹 ∈ ( ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ) Cn_u ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ) ) )
15		eqid	⊢ ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) )
16		eqid	⊢ ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) = ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) )
17		oveq2	⊢ ( 𝑎 = 𝑐 → ( 0 [,) 𝑎 ) = ( 0 [,) 𝑐 ) )
18	17	imaeq2d	⊢ ( 𝑎 = 𝑐 → ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) = ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) )
19	18	cbvmptv	⊢ ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑐 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) )
20	19	rneqi	⊢ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) = ran ( 𝑐 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) )
21	20	metust	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐶 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ) ∈ ( UnifOn ‘ 𝑋 ) )
22	3 5 21	syl2anc	⊢ ( 𝜑 → ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ) ∈ ( UnifOn ‘ 𝑋 ) )
23		oveq2	⊢ ( 𝑏 = 𝑑 → ( 0 [,) 𝑏 ) = ( 0 [,) 𝑑 ) )
24	23	imaeq2d	⊢ ( 𝑏 = 𝑑 → ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) )
25	24	cbvmptv	⊢ ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) = ( 𝑑 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) )
26	25	rneqi	⊢ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) = ran ( 𝑑 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) )
27	26	metust	⊢ ( ( 𝑌 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑌 ) ) → ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∈ ( UnifOn ‘ 𝑌 ) )
28	4 6 27	syl2anc	⊢ ( 𝜑 → ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ∈ ( UnifOn ‘ 𝑌 ) )
29		oveq2	⊢ ( 𝑎 = 𝑒 → ( 0 [,) 𝑎 ) = ( 0 [,) 𝑒 ) )
30	29	imaeq2d	⊢ ( 𝑎 = 𝑒 → ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) = ( ^◡ 𝐶 “ ( 0 [,) 𝑒 ) ) )
31	30	cbvmptv	⊢ ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑒 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑒 ) ) )
32	31	rneqi	⊢ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) = ran ( 𝑒 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑒 ) ) )
33	32	metustfbas	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐶 ∈ ( PsMet ‘ 𝑋 ) ) → ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
34	3 5 33	syl2anc	⊢ ( 𝜑 → ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
35		oveq2	⊢ ( 𝑏 = 𝑓 → ( 0 [,) 𝑏 ) = ( 0 [,) 𝑓 ) )
36	35	imaeq2d	⊢ ( 𝑏 = 𝑓 → ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑓 ) ) )
37	36	cbvmptv	⊢ ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) = ( 𝑓 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑓 ) ) )
38	37	rneqi	⊢ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) = ran ( 𝑓 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑓 ) ) )
39	38	metustfbas	⊢ ( ( 𝑌 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑌 ) ) → ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ∈ ( fBas ‘ ( 𝑌 × 𝑌 ) ) )
40	4 6 39	syl2anc	⊢ ( 𝜑 → ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ∈ ( fBas ‘ ( 𝑌 × 𝑌 ) ) )
41	15 16 22 28 34 40	isucn2	⊢ ( 𝜑 → ( 𝐹 ∈ ( ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ) Cn_u ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑣 ∈ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ∃ 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) ) )
42	14 41	bitrd	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑈 Cn_u 𝑉 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑣 ∈ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ∃ 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) ) )
43		eqid	⊢ ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) )
44		oveq2	⊢ ( 𝑓 = 𝑑 → ( 0 [,) 𝑓 ) = ( 0 [,) 𝑑 ) )
45	44	imaeq2d	⊢ ( 𝑓 = 𝑑 → ( ^◡ 𝐷 “ ( 0 [,) 𝑓 ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) )
46	45	rspceeqv	⊢ ( ( 𝑑 ∈ ℝ⁺ ∧ ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) → ∃ 𝑓 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑓 ) ) )
47	43 46	mpan2	⊢ ( 𝑑 ∈ ℝ⁺ → ∃ 𝑓 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑓 ) ) )
48	47	adantl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℝ⁺ ) → ∃ 𝑓 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑓 ) ) )
49	38	metustel	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑌 ) → ( ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∈ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ↔ ∃ 𝑓 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑓 ) ) ) )
50	6 49	syl	⊢ ( 𝜑 → ( ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∈ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ↔ ∃ 𝑓 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑓 ) ) ) )
51	50	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∈ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ↔ ∃ 𝑓 ∈ ℝ⁺ ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) = ( ^◡ 𝐷 “ ( 0 [,) 𝑓 ) ) ) )
52	48 51	mpbird	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℝ⁺ ) → ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∈ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) )
53	26	metustel	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑌 ) → ( 𝑣 ∈ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ↔ ∃ 𝑑 ∈ ℝ⁺ 𝑣 = ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) )
54	6 53	syl	⊢ ( 𝜑 → ( 𝑣 ∈ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ↔ ∃ 𝑑 ∈ ℝ⁺ 𝑣 = ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) )
55		simpr	⊢ ( ( 𝜑 ∧ 𝑣 = ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) → 𝑣 = ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) )
56	55	breqd	⊢ ( ( 𝜑 ∧ 𝑣 = ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) )
57	56	imbi2d	⊢ ( ( 𝜑 ∧ 𝑣 = ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) → ( ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
58	57	ralbidv	⊢ ( ( 𝜑 ∧ 𝑣 = ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
59	58	rexralbidv	⊢ ( ( 𝜑 ∧ 𝑣 = ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) → ( ∃ 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
60	52 54 59	ralxfr2d	⊢ ( 𝜑 → ( ∀ 𝑣 ∈ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ∃ 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑑 ∈ ℝ⁺ ∃ 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
61		eqid	⊢ ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) = ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) )
62		oveq2	⊢ ( 𝑒 = 𝑐 → ( 0 [,) 𝑒 ) = ( 0 [,) 𝑐 ) )
63	62	imaeq2d	⊢ ( 𝑒 = 𝑐 → ( ^◡ 𝐶 “ ( 0 [,) 𝑒 ) ) = ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) )
64	63	rspceeqv	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) = ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) ) → ∃ 𝑒 ∈ ℝ⁺ ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) = ( ^◡ 𝐶 “ ( 0 [,) 𝑒 ) ) )
65	61 64	mpan2	⊢ ( 𝑐 ∈ ℝ⁺ → ∃ 𝑒 ∈ ℝ⁺ ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) = ( ^◡ 𝐶 “ ( 0 [,) 𝑒 ) ) )
66	65	adantl	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℝ⁺ ) → ∃ 𝑒 ∈ ℝ⁺ ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) = ( ^◡ 𝐶 “ ( 0 [,) 𝑒 ) ) )
67	32	metustel	⊢ ( 𝐶 ∈ ( PsMet ‘ 𝑋 ) → ( ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑒 ∈ ℝ⁺ ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) = ( ^◡ 𝐶 “ ( 0 [,) 𝑒 ) ) ) )
68	5 67	syl	⊢ ( 𝜑 → ( ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑒 ∈ ℝ⁺ ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) = ( ^◡ 𝐶 “ ( 0 [,) 𝑒 ) ) ) )
69	68	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℝ⁺ ) → ( ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑒 ∈ ℝ⁺ ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) = ( ^◡ 𝐶 “ ( 0 [,) 𝑒 ) ) ) )
70	66 69	mpbird	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℝ⁺ ) → ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) )
71	20	metustel	⊢ ( 𝐶 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑐 ∈ ℝ⁺ 𝑢 = ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) ) )
72	5 71	syl	⊢ ( 𝜑 → ( 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑐 ∈ ℝ⁺ 𝑢 = ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) ) )
73		simpr	⊢ ( ( 𝜑 ∧ 𝑢 = ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) ) → 𝑢 = ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) )
74	73	breqd	⊢ ( ( 𝜑 ∧ 𝑢 = ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) ) → ( 𝑥 𝑢 𝑦 ↔ 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 ) )
75	74	imbi1d	⊢ ( ( 𝜑 ∧ 𝑢 = ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) ) → ( ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
76	75	2ralbidv	⊢ ( ( 𝜑 ∧ 𝑢 = ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
77	70 72 76	rexxfr2d	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
78	77	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑑 ∈ ℝ⁺ ∃ 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑑 ∈ ℝ⁺ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
79	60 78	bitrd	⊢ ( 𝜑 → ( ∀ 𝑣 ∈ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ∃ 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑑 ∈ ℝ⁺ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
80	79	adantr	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑣 ∈ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ∃ 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑑 ∈ ℝ⁺ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ) )
81	5	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐶 ∈ ( PsMet ‘ 𝑋 ) )
82		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑐 ∈ ℝ⁺ )
83		simprr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
84		simprl	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
85		elbl4	⊢ ( ( ( 𝐶 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 ∈ ( 𝑦 ( ball ‘ 𝐶 ) 𝑐 ) ↔ 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 ) )
86		rpxr	⊢ ( 𝑐 ∈ ℝ⁺ → 𝑐 ∈ ℝ^* )
87		elbl3ps	⊢ ( ( ( 𝐶 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑐 ∈ ℝ^* ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 ∈ ( 𝑦 ( ball ‘ 𝐶 ) 𝑐 ) ↔ ( 𝑥 𝐶 𝑦 ) < 𝑐 ) )
88	86 87	sylanl2	⊢ ( ( ( 𝐶 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 ∈ ( 𝑦 ( ball ‘ 𝐶 ) 𝑐 ) ↔ ( 𝑥 𝐶 𝑦 ) < 𝑐 ) )
89	85 88	bitr3d	⊢ ( ( ( 𝐶 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 ↔ ( 𝑥 𝐶 𝑦 ) < 𝑐 ) )
90	81 82 83 84 89	syl22anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 ↔ ( 𝑥 𝐶 𝑦 ) < 𝑐 ) )
91	6	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐷 ∈ ( PsMet ‘ 𝑌 ) )
92		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑑 ∈ ℝ⁺ )
93		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
94	93 83	ffvelcdmd	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 )
95	93 84	ffvelcdmd	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑌 )
96		elbl4	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ 𝐷 ) 𝑑 ) ↔ ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) )
97		rpxr	⊢ ( 𝑑 ∈ ℝ⁺ → 𝑑 ∈ ℝ^* )
98		elbl3ps	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑌 ) ∧ 𝑑 ∈ ℝ^* ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ 𝐷 ) 𝑑 ) ↔ ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) )
99	97 98	sylanl2	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ 𝐷 ) 𝑑 ) ↔ ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) )
100	96 99	bitr3d	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) )
101	91 92 94 95 100	syl22anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) )
102	90 101	imbi12d	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝑥 𝐶 𝑦 ) < 𝑐 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) ) )
103	102	2ralbidva	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑐 ∈ ℝ⁺ ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐶 𝑦 ) < 𝑐 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) ) )
104	103	rexbidva	⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐶 𝑦 ) < 𝑐 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) ) )
105	104	ralbidva	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑑 ∈ ℝ⁺ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( ^◡ 𝐶 “ ( 0 [,) 𝑐 ) ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( ^◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑑 ∈ ℝ⁺ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐶 𝑦 ) < 𝑐 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) ) )
106	80 105	bitrd	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑣 ∈ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ∃ 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑑 ∈ ℝ⁺ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐶 𝑦 ) < 𝑐 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) ) )
107	106	pm5.32da	⊢ ( 𝜑 → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑣 ∈ ran ( 𝑏 ∈ ℝ⁺ ↦ ( ^◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ∃ 𝑢 ∈ ran ( 𝑎 ∈ ℝ⁺ ↦ ( ^◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑑 ∈ ℝ⁺ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐶 𝑦 ) < 𝑐 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) ) ) )
108	42 107	bitrd	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑈 Cn_u 𝑉 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑑 ∈ ℝ⁺ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐶 𝑦 ) < 𝑐 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) ) ) )

Metamath Proof Explorer

Theorem metucn

Proof