Metamath Proof Explorer

Theorem 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 ( 𝜑 → ( 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐶 𝑦 ) < 𝑐 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) ) ) )

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 syl5eq ⊢ ( 𝜑 → 𝑈 = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ) )
10 metuval ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑌 ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) )
11 6 10 syl ⊢ ( 𝜑 → ( metUnif ‘ 𝐷 ) = ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) )
12 2 11 syl5eq ⊢ ( 𝜑 → 𝑉 = ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) )
13 9 12 oveq12d ⊢ ( 𝜑 → ( 𝑈 Cnu 𝑉 ) = ( ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ) Cnu ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ) )
14 13 eleq2d ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) ↔ 𝐹 ∈ ( ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ) Cnu ( ( 𝑌 × 𝑌 ) 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 [,) 𝑎 ) ) ) ) Cnu ( ( 𝑌 × 𝑌 ) filGen ran ( 𝑏 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑣 ∈ ran ( 𝑏 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑏 ) ) ) ∃ 𝑢 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐶 “ ( 0 [,) 𝑎 ) ) ) ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑢 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) ) )
42 14 41 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑣 ∈ 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 ffvelrnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 )
95 93 84 ffvelrnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑌 )
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 ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐶 𝑦 ) < 𝑐 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) < 𝑑 ) ) ) )