Metamath Proof Explorer


Theorem heicant

Description: Heine-Cantor theorem: a continuous mapping between metric spaces whose domain is compact is uniformly continuous. Theorem on Rosenlicht p. 80. (Contributed by Brendan Leahy, 13-Aug-2018) (Proof shortened by AV, 27-Sep-2020)

Ref Expression
Hypotheses heicant.c ( 𝜑𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
heicant.d ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
heicant.j ( 𝜑 → ( MetOpen ‘ 𝐶 ) ∈ Comp )
heicant.x ( 𝜑𝑋 ≠ ∅ )
heicant.y ( 𝜑𝑌 ≠ ∅ )
Assertion heicant ( 𝜑 → ( ( metUnif ‘ 𝐶 ) Cnu ( metUnif ‘ 𝐷 ) ) = ( ( MetOpen ‘ 𝐶 ) Cn ( MetOpen ‘ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 heicant.c ( 𝜑𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
2 heicant.d ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
3 heicant.j ( 𝜑 → ( MetOpen ‘ 𝐶 ) ∈ Comp )
4 heicant.x ( 𝜑𝑋 ≠ ∅ )
5 heicant.y ( 𝜑𝑌 ≠ ∅ )
6 breq2 ( 𝑑 = 𝑦 → ( ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ↔ ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) )
7 6 imbi2d ( 𝑑 = 𝑦 → ( ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ↔ ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ) )
8 7 2ralbidv ( 𝑑 = 𝑦 → ( ∀ 𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ↔ ∀ 𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ) )
9 8 rexbidv ( 𝑑 = 𝑦 → ( ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ↔ ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ) )
10 9 cbvralvw ( ∀ 𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ↔ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) )
11 r19.12 ( ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) → ∀ 𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) )
12 11 ralimi ( ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) → ∀ 𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) )
13 10 12 sylbi ( ∀ 𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) → ∀ 𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) )
14 rphalfcl ( 𝑑 ∈ ℝ+ → ( 𝑑 / 2 ) ∈ ℝ+ )
15 breq2 ( 𝑦 = ( 𝑑 / 2 ) → ( ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ↔ ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) )
16 15 imbi2d ( 𝑦 = ( 𝑑 / 2 ) → ( ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ↔ ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) )
17 16 ralbidv ( 𝑦 = ( 𝑑 / 2 ) → ( ∀ 𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) )
18 17 rexbidv ( 𝑦 = ( 𝑑 / 2 ) → ( ∃ 𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) )
19 18 ralbidv ( 𝑦 = ( 𝑑 / 2 ) → ( ∀ 𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) )
20 19 rspcva ( ( ( 𝑑 / 2 ) ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ) → ∀ 𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) )
21 3 ad3antrrr ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ∀ 𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( MetOpen ‘ 𝐶 ) ∈ Comp )
22 1 ad2antrr ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
23 22 anim1i ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥𝑋 ) )
24 rphalfcl ( 𝑧 ∈ ℝ+ → ( 𝑧 / 2 ) ∈ ℝ+ )
25 24 rpxrd ( 𝑧 ∈ ℝ+ → ( 𝑧 / 2 ) ∈ ℝ* )
26 eqid ( MetOpen ‘ 𝐶 ) = ( MetOpen ‘ 𝐶 )
27 26 blopn ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥𝑋 ∧ ( 𝑧 / 2 ) ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) ∈ ( MetOpen ‘ 𝐶 ) )
28 27 3expa ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥𝑋 ) ∧ ( 𝑧 / 2 ) ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) ∈ ( MetOpen ‘ 𝐶 ) )
29 23 25 28 syl2an ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥𝑋 ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) ∈ ( MetOpen ‘ 𝐶 ) )
30 29 adantr ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥𝑋 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) ∈ ( MetOpen ‘ 𝐶 ) )
31 24 rpgt0d ( 𝑧 ∈ ℝ+ → 0 < ( 𝑧 / 2 ) )
32 25 31 jca ( 𝑧 ∈ ℝ+ → ( ( 𝑧 / 2 ) ∈ ℝ* ∧ 0 < ( 𝑧 / 2 ) ) )
33 xblcntr ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥𝑋 ∧ ( ( 𝑧 / 2 ) ∈ ℝ* ∧ 0 < ( 𝑧 / 2 ) ) ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) )
34 33 3expa ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥𝑋 ) ∧ ( ( 𝑧 / 2 ) ∈ ℝ* ∧ 0 < ( 𝑧 / 2 ) ) ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) )
35 23 32 34 syl2an ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥𝑋 ) ∧ 𝑧 ∈ ℝ+ ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) )
36 35 adantr ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥𝑋 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) )
37 opelxpi ( ( 𝑥𝑋 ∧ ( 𝑧 / 2 ) ∈ ℝ+ ) → ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ ∈ ( 𝑋 × ℝ+ ) )
38 24 37 sylan2 ( ( 𝑥𝑋𝑧 ∈ ℝ+ ) → ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ ∈ ( 𝑋 × ℝ+ ) )
39 38 ad4ant23 ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥𝑋 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ ∈ ( 𝑋 × ℝ+ ) )
40 rpcn ( 𝑧 ∈ ℝ+𝑧 ∈ ℂ )
41 40 2halvesd ( 𝑧 ∈ ℝ+ → ( ( 𝑧 / 2 ) + ( 𝑧 / 2 ) ) = 𝑧 )
42 41 breq2d ( 𝑧 ∈ ℝ+ → ( ( 𝑥 𝐶 𝑐 ) < ( ( 𝑧 / 2 ) + ( 𝑧 / 2 ) ) ↔ ( 𝑥 𝐶 𝑐 ) < 𝑧 ) )
43 42 imbi1d ( 𝑧 ∈ ℝ+ → ( ( ( 𝑥 𝐶 𝑐 ) < ( ( 𝑧 / 2 ) + ( 𝑧 / 2 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ↔ ( ( 𝑥 𝐶 𝑐 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) )
44 43 ralbidv ( 𝑧 ∈ ℝ+ → ( ∀ 𝑐𝑋 ( ( 𝑥 𝐶 𝑐 ) < ( ( 𝑧 / 2 ) + ( 𝑧 / 2 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ↔ ∀ 𝑐𝑋 ( ( 𝑥 𝐶 𝑐 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) )
45 oveq2 ( 𝑐 = 𝑤 → ( 𝑥 𝐶 𝑐 ) = ( 𝑥 𝐶 𝑤 ) )
46 45 breq1d ( 𝑐 = 𝑤 → ( ( 𝑥 𝐶 𝑐 ) < 𝑧 ↔ ( 𝑥 𝐶 𝑤 ) < 𝑧 ) )
47 fveq2 ( 𝑐 = 𝑤 → ( 𝑓𝑐 ) = ( 𝑓𝑤 ) )
48 47 oveq2d ( 𝑐 = 𝑤 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) = ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) )
49 48 breq1d ( 𝑐 = 𝑤 → ( ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ↔ ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) )
50 46 49 imbi12d ( 𝑐 = 𝑤 → ( ( ( 𝑥 𝐶 𝑐 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ↔ ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) )
51 50 cbvralvw ( ∀ 𝑐𝑋 ( ( 𝑥 𝐶 𝑐 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ↔ ∀ 𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) )
52 44 51 bitrdi ( 𝑧 ∈ ℝ+ → ( ∀ 𝑐𝑋 ( ( 𝑥 𝐶 𝑐 ) < ( ( 𝑧 / 2 ) + ( 𝑧 / 2 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ↔ ∀ 𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) )
53 52 biimpar ( ( 𝑧 ∈ ℝ+ ∧ ∀ 𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ∀ 𝑐𝑋 ( ( 𝑥 𝐶 𝑐 ) < ( ( 𝑧 / 2 ) + ( 𝑧 / 2 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) )
54 53 adantll ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥𝑋 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ∀ 𝑐𝑋 ( ( 𝑥 𝐶 𝑐 ) < ( ( 𝑧 / 2 ) + ( 𝑧 / 2 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) )
55 vex 𝑥 ∈ V
56 ovex ( 𝑧 / 2 ) ∈ V
57 55 56 op1std ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( 1st𝑝 ) = 𝑥 )
58 55 56 op2ndd ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( 2nd𝑝 ) = ( 𝑧 / 2 ) )
59 57 58 oveq12d ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) = ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) )
60 59 eqcomd ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) )
61 60 biantrurd ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ↔ ( ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) )
62 57 oveq1d ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( ( 1st𝑝 ) 𝐶 𝑐 ) = ( 𝑥 𝐶 𝑐 ) )
63 58 58 oveq12d ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) = ( ( 𝑧 / 2 ) + ( 𝑧 / 2 ) ) )
64 62 63 breq12d ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) ↔ ( 𝑥 𝐶 𝑐 ) < ( ( 𝑧 / 2 ) + ( 𝑧 / 2 ) ) ) )
65 57 fveq2d ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( 𝑓 ‘ ( 1st𝑝 ) ) = ( 𝑓𝑥 ) )
66 65 oveq1d ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) = ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) )
67 66 breq1d ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ↔ ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) )
68 64 67 imbi12d ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ↔ ( ( 𝑥 𝐶 𝑐 ) < ( ( 𝑧 / 2 ) + ( 𝑧 / 2 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) )
69 68 ralbidv ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ↔ ∀ 𝑐𝑋 ( ( 𝑥 𝐶 𝑐 ) < ( ( 𝑧 / 2 ) + ( 𝑧 / 2 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) )
70 61 69 bitr3d ( 𝑝 = ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ → ( ( ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ↔ ∀ 𝑐𝑋 ( ( 𝑥 𝐶 𝑐 ) < ( ( 𝑧 / 2 ) + ( 𝑧 / 2 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) )
71 70 rspcev ( ( ⟨ 𝑥 , ( 𝑧 / 2 ) ⟩ ∈ ( 𝑋 × ℝ+ ) ∧ ∀ 𝑐𝑋 ( ( 𝑥 𝐶 𝑐 ) < ( ( 𝑧 / 2 ) + ( 𝑧 / 2 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) → ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) )
72 39 54 71 syl2anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥𝑋 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) )
73 eleq2 ( 𝑏 = ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) → ( 𝑥𝑏𝑥 ∈ ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) ) )
74 eqeq1 ( 𝑏 = ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) → ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ↔ ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ) )
75 74 anbi1d ( 𝑏 = ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) → ( ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ↔ ( ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) )
76 75 rexbidv ( 𝑏 = ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) → ( ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ↔ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) )
77 73 76 anbi12d ( 𝑏 = ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) → ( ( 𝑥𝑏 ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ↔ ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ) )
78 77 rspcev ( ( ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) ∈ ( MetOpen ‘ 𝐶 ) ∧ ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( ( 𝑥 ( ball ‘ 𝐶 ) ( 𝑧 / 2 ) ) = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ) → ∃ 𝑏 ∈ ( MetOpen ‘ 𝐶 ) ( 𝑥𝑏 ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) )
79 30 36 72 78 syl12anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥𝑋 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ∀ 𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ∃ 𝑏 ∈ ( MetOpen ‘ 𝐶 ) ( 𝑥𝑏 ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) )
80 79 rexlimdva2 ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → ( ∃ 𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) → ∃ 𝑏 ∈ ( MetOpen ‘ 𝐶 ) ( 𝑥𝑏 ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ) )
81 80 ralimdva ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) → ( ∀ 𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) → ∀ 𝑥𝑋𝑏 ∈ ( MetOpen ‘ 𝐶 ) ( 𝑥𝑏 ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ) )
82 81 imp ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ∀ 𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ∀ 𝑥𝑋𝑏 ∈ ( MetOpen ‘ 𝐶 ) ( 𝑥𝑏 ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) )
83 26 mopnuni ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ( MetOpen ‘ 𝐶 ) )
84 1 83 syl ( 𝜑𝑋 = ( MetOpen ‘ 𝐶 ) )
85 84 raleqdv ( 𝜑 → ( ∀ 𝑥𝑋𝑏 ∈ ( MetOpen ‘ 𝐶 ) ( 𝑥𝑏 ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ↔ ∀ 𝑥 ( MetOpen ‘ 𝐶 ) ∃ 𝑏 ∈ ( MetOpen ‘ 𝐶 ) ( 𝑥𝑏 ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ) )
86 85 ad3antrrr ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ∀ 𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ∀ 𝑥𝑋𝑏 ∈ ( MetOpen ‘ 𝐶 ) ( 𝑥𝑏 ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ↔ ∀ 𝑥 ( MetOpen ‘ 𝐶 ) ∃ 𝑏 ∈ ( MetOpen ‘ 𝐶 ) ( 𝑥𝑏 ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ) )
87 82 86 mpbid ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ∀ 𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ∀ 𝑥 ( MetOpen ‘ 𝐶 ) ∃ 𝑏 ∈ ( MetOpen ‘ 𝐶 ) ( 𝑥𝑏 ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) )
88 eqid ( MetOpen ‘ 𝐶 ) = ( MetOpen ‘ 𝐶 )
89 fveq2 ( 𝑝 = ( 𝑔𝑏 ) → ( 1st𝑝 ) = ( 1st ‘ ( 𝑔𝑏 ) ) )
90 fveq2 ( 𝑝 = ( 𝑔𝑏 ) → ( 2nd𝑝 ) = ( 2nd ‘ ( 𝑔𝑏 ) ) )
91 89 90 oveq12d ( 𝑝 = ( 𝑔𝑏 ) → ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
92 91 eqeq2d ( 𝑝 = ( 𝑔𝑏 ) → ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ↔ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) )
93 89 oveq1d ( 𝑝 = ( 𝑔𝑏 ) → ( ( 1st𝑝 ) 𝐶 𝑐 ) = ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) )
94 90 90 oveq12d ( 𝑝 = ( 𝑔𝑏 ) → ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) = ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
95 93 94 breq12d ( 𝑝 = ( 𝑔𝑏 ) → ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) ↔ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) )
96 89 fveq2d ( 𝑝 = ( 𝑔𝑏 ) → ( 𝑓 ‘ ( 1st𝑝 ) ) = ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) )
97 96 oveq1d ( 𝑝 = ( 𝑔𝑏 ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) = ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) )
98 97 breq1d ( 𝑝 = ( 𝑔𝑏 ) → ( ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ↔ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) )
99 95 98 imbi12d ( 𝑝 = ( 𝑔𝑏 ) → ( ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ↔ ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) )
100 99 ralbidv ( 𝑝 = ( 𝑔𝑏 ) → ( ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ↔ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) )
101 92 100 anbi12d ( 𝑝 = ( 𝑔𝑏 ) → ( ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ↔ ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) )
102 88 101 cmpcovf ( ( ( MetOpen ‘ 𝐶 ) ∈ Comp ∧ ∀ 𝑥 ( MetOpen ‘ 𝐶 ) ∃ 𝑏 ∈ ( MetOpen ‘ 𝐶 ) ( 𝑥𝑏 ∧ ∃ 𝑝 ∈ ( 𝑋 × ℝ+ ) ( 𝑏 = ( ( 1st𝑝 ) ( ball ‘ 𝐶 ) ( 2nd𝑝 ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st𝑝 ) 𝐶 𝑐 ) < ( ( 2nd𝑝 ) + ( 2nd𝑝 ) ) → ( ( 𝑓 ‘ ( 1st𝑝 ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ) → ∃ 𝑠 ∈ ( 𝒫 ( MetOpen ‘ 𝐶 ) ∩ Fin ) ( ( MetOpen ‘ 𝐶 ) = 𝑠 ∧ ∃ 𝑔 ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ) )
103 21 87 102 syl2anc ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ ∀ 𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ∃ 𝑠 ∈ ( 𝒫 ( MetOpen ‘ 𝐶 ) ∩ Fin ) ( ( MetOpen ‘ 𝐶 ) = 𝑠 ∧ ∃ 𝑔 ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ) )
104 103 ex ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) → ( ∀ 𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) → ∃ 𝑠 ∈ ( 𝒫 ( MetOpen ‘ 𝐶 ) ∩ Fin ) ( ( MetOpen ‘ 𝐶 ) = 𝑠 ∧ ∃ 𝑔 ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ) ) )
105 elinel2 ( 𝑠 ∈ ( 𝒫 ( MetOpen ‘ 𝐶 ) ∩ Fin ) → 𝑠 ∈ Fin )
106 simpll ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) → 𝜑 )
107 106 anim1i ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) → ( 𝜑𝑠 ∈ Fin ) )
108 frn ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) → ran 𝑔 ⊆ ( 𝑋 × ℝ+ ) )
109 rnss ( ran 𝑔 ⊆ ( 𝑋 × ℝ+ ) → ran ran 𝑔 ⊆ ran ( 𝑋 × ℝ+ ) )
110 108 109 syl ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) → ran ran 𝑔 ⊆ ran ( 𝑋 × ℝ+ ) )
111 rnxpss ran ( 𝑋 × ℝ+ ) ⊆ ℝ+
112 110 111 sstrdi ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) → ran ran 𝑔 ⊆ ℝ+ )
113 112 adantl ( ( ( ( 𝜑𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → ran ran 𝑔 ⊆ ℝ+ )
114 simplr ( ( ( 𝜑𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) → 𝑠 ∈ Fin )
115 ffun ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) → Fun 𝑔 )
116 vex 𝑔 ∈ V
117 116 fundmen ( Fun 𝑔 → dom 𝑔𝑔 )
118 117 ensymd ( Fun 𝑔𝑔 ≈ dom 𝑔 )
119 115 118 syl ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) → 𝑔 ≈ dom 𝑔 )
120 fdm ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) → dom 𝑔 = 𝑠 )
121 119 120 breqtrd ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) → 𝑔𝑠 )
122 enfii ( ( 𝑠 ∈ Fin ∧ 𝑔𝑠 ) → 𝑔 ∈ Fin )
123 121 122 sylan2 ( ( 𝑠 ∈ Fin ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → 𝑔 ∈ Fin )
124 rnfi ( 𝑔 ∈ Fin → ran 𝑔 ∈ Fin )
125 rnfi ( ran 𝑔 ∈ Fin → ran ran 𝑔 ∈ Fin )
126 123 124 125 3syl ( ( 𝑠 ∈ Fin ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → ran ran 𝑔 ∈ Fin )
127 114 126 sylan ( ( ( ( 𝜑𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → ran ran 𝑔 ∈ Fin )
128 120 adantl ( ( ( 𝜑 ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → dom 𝑔 = 𝑠 )
129 eqtr ( ( 𝑋 = ( MetOpen ‘ 𝐶 ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) → 𝑋 = 𝑠 )
130 84 129 sylan ( ( 𝜑 ( MetOpen ‘ 𝐶 ) = 𝑠 ) → 𝑋 = 𝑠 )
131 4 adantr ( ( 𝜑 ( MetOpen ‘ 𝐶 ) = 𝑠 ) → 𝑋 ≠ ∅ )
132 130 131 eqnetrrd ( ( 𝜑 ( MetOpen ‘ 𝐶 ) = 𝑠 ) → 𝑠 ≠ ∅ )
133 unieq ( 𝑠 = ∅ → 𝑠 = ∅ )
134 uni0 ∅ = ∅
135 133 134 eqtrdi ( 𝑠 = ∅ → 𝑠 = ∅ )
136 135 necon3i ( 𝑠 ≠ ∅ → 𝑠 ≠ ∅ )
137 132 136 syl ( ( 𝜑 ( MetOpen ‘ 𝐶 ) = 𝑠 ) → 𝑠 ≠ ∅ )
138 137 adantr ( ( ( 𝜑 ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → 𝑠 ≠ ∅ )
139 128 138 eqnetrd ( ( ( 𝜑 ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → dom 𝑔 ≠ ∅ )
140 dm0rn0 ( dom 𝑔 = ∅ ↔ ran 𝑔 = ∅ )
141 140 necon3bii ( dom 𝑔 ≠ ∅ ↔ ran 𝑔 ≠ ∅ )
142 139 141 sylib ( ( ( 𝜑 ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → ran 𝑔 ≠ ∅ )
143 relxp Rel ( 𝑋 × ℝ+ )
144 relss ( ran 𝑔 ⊆ ( 𝑋 × ℝ+ ) → ( Rel ( 𝑋 × ℝ+ ) → Rel ran 𝑔 ) )
145 108 143 144 mpisyl ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) → Rel ran 𝑔 )
146 relrn0 ( Rel ran 𝑔 → ( ran 𝑔 = ∅ ↔ ran ran 𝑔 = ∅ ) )
147 146 necon3bid ( Rel ran 𝑔 → ( ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅ ) )
148 145 147 syl ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) → ( ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅ ) )
149 148 adantl ( ( ( 𝜑 ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → ( ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅ ) )
150 142 149 mpbid ( ( ( 𝜑 ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → ran ran 𝑔 ≠ ∅ )
151 150 adantllr ( ( ( ( 𝜑𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → ran ran 𝑔 ≠ ∅ )
152 rpssre + ⊆ ℝ
153 113 152 sstrdi ( ( ( ( 𝜑𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → ran ran 𝑔 ⊆ ℝ )
154 ltso < Or ℝ
155 fiinfcl ( ( < Or ℝ ∧ ( ran ran 𝑔 ∈ Fin ∧ ran ran 𝑔 ≠ ∅ ∧ ran ran 𝑔 ⊆ ℝ ) ) → inf ( ran ran 𝑔 , ℝ , < ) ∈ ran ran 𝑔 )
156 154 155 mpan ( ( ran ran 𝑔 ∈ Fin ∧ ran ran 𝑔 ≠ ∅ ∧ ran ran 𝑔 ⊆ ℝ ) → inf ( ran ran 𝑔 , ℝ , < ) ∈ ran ran 𝑔 )
157 127 151 153 156 syl3anc ( ( ( ( 𝜑𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → inf ( ran ran 𝑔 , ℝ , < ) ∈ ran ran 𝑔 )
158 113 157 sseldd ( ( ( ( 𝜑𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → inf ( ran ran 𝑔 , ℝ , < ) ∈ ℝ+ )
159 107 158 sylanl1 ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → inf ( ran ran 𝑔 , ℝ , < ) ∈ ℝ+ )
160 159 adantr ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) → inf ( ran ran 𝑔 , ℝ , < ) ∈ ℝ+ )
161 84 ad3antrrr ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) → 𝑋 = ( MetOpen ‘ 𝐶 ) )
162 161 anim1i ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) → ( 𝑋 = ( MetOpen ‘ 𝐶 ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) )
163 162 ad2antrr ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) → ( 𝑋 = ( MetOpen ‘ 𝐶 ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) )
164 simpl ( ( 𝑥𝑋𝑤𝑋 ) → 𝑥𝑋 )
165 129 eleq2d ( ( 𝑋 = ( MetOpen ‘ 𝐶 ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) → ( 𝑥𝑋𝑥 𝑠 ) )
166 eluni2 ( 𝑥 𝑠 ↔ ∃ 𝑏𝑠 𝑥𝑏 )
167 165 166 bitrdi ( ( 𝑋 = ( MetOpen ‘ 𝐶 ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) → ( 𝑥𝑋 ↔ ∃ 𝑏𝑠 𝑥𝑏 ) )
168 167 biimpa ( ( ( 𝑋 = ( MetOpen ‘ 𝐶 ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑥𝑋 ) → ∃ 𝑏𝑠 𝑥𝑏 )
169 163 164 168 syl2an ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → ∃ 𝑏𝑠 𝑥𝑏 )
170 nfv 𝑏 ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) )
171 nfra1 𝑏𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) )
172 170 171 nfan 𝑏 ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) )
173 nfv 𝑏 ( 𝑥𝑋𝑤𝑋 )
174 172 173 nfan 𝑏 ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) )
175 nfv 𝑏 ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 )
176 rspa ( ( ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ∧ 𝑏𝑠 ) → ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) )
177 oveq2 ( 𝑐 = 𝑥 → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) = ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) )
178 177 breq1d ( 𝑐 = 𝑥 → ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ↔ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) )
179 fveq2 ( 𝑐 = 𝑥 → ( 𝑓𝑐 ) = ( 𝑓𝑥 ) )
180 179 oveq2d ( 𝑐 = 𝑥 → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) = ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) )
181 180 breq1d ( 𝑐 = 𝑥 → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ↔ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ) )
182 178 181 imbi12d ( 𝑐 = 𝑥 → ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ↔ ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ) ) )
183 182 rspcva ( ( 𝑥𝑋 ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ) )
184 oveq2 ( 𝑐 = 𝑤 → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) = ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) )
185 184 breq1d ( 𝑐 = 𝑤 → ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ↔ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) )
186 47 oveq2d ( 𝑐 = 𝑤 → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) = ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) )
187 186 breq1d ( 𝑐 = 𝑤 → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ↔ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) )
188 185 187 imbi12d ( 𝑐 = 𝑤 → ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ↔ ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) )
189 188 rspcva ( ( 𝑤𝑋 ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) )
190 183 189 anim12i ( ( ( 𝑥𝑋 ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ∧ ( 𝑤𝑋 ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) → ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ) ∧ ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) )
191 190 anandirs ( ( ( 𝑥𝑋𝑤𝑋 ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ) ∧ ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) )
192 anim12 ( ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ) ∧ ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) )
193 191 192 syl ( ( ( 𝑥𝑋𝑤𝑋 ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) )
194 193 adantrl ( ( ( 𝑥𝑋𝑤𝑋 ) ∧ ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) → ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) )
195 194 ad4ant23 ( ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) )
196 simpll ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) → ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) )
197 196 anim1i ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) )
198 197 anim1i ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) )
199 112 152 sstrdi ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) → ran ran 𝑔 ⊆ ℝ )
200 199 adantr ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → ran ran 𝑔 ⊆ ℝ )
201 0re 0 ∈ ℝ
202 rpge0 ( 𝑦 ∈ ℝ+ → 0 ≤ 𝑦 )
203 202 rgen 𝑦 ∈ ℝ+ 0 ≤ 𝑦
204 ssralv ( ran ran 𝑔 ⊆ ℝ+ → ( ∀ 𝑦 ∈ ℝ+ 0 ≤ 𝑦 → ∀ 𝑦 ∈ ran ran 𝑔 0 ≤ 𝑦 ) )
205 112 203 204 mpisyl ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) → ∀ 𝑦 ∈ ran ran 𝑔 0 ≤ 𝑦 )
206 breq1 ( 𝑥 = 0 → ( 𝑥𝑦 ↔ 0 ≤ 𝑦 ) )
207 206 ralbidv ( 𝑥 = 0 → ( ∀ 𝑦 ∈ ran ran 𝑔 𝑥𝑦 ↔ ∀ 𝑦 ∈ ran ran 𝑔 0 ≤ 𝑦 ) )
208 207 rspcev ( ( 0 ∈ ℝ ∧ ∀ 𝑦 ∈ ran ran 𝑔 0 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ran 𝑔 𝑥𝑦 )
209 201 205 208 sylancr ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ran 𝑔 𝑥𝑦 )
210 209 adantr ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ran 𝑔 𝑥𝑦 )
211 145 adantr ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → Rel ran 𝑔 )
212 ffn ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) → 𝑔 Fn 𝑠 )
213 fnfvelrn ( ( 𝑔 Fn 𝑠𝑏𝑠 ) → ( 𝑔𝑏 ) ∈ ran 𝑔 )
214 212 213 sylan ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → ( 𝑔𝑏 ) ∈ ran 𝑔 )
215 2ndrn ( ( Rel ran 𝑔 ∧ ( 𝑔𝑏 ) ∈ ran 𝑔 ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ran ran 𝑔 )
216 211 214 215 syl2anc ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ran ran 𝑔 )
217 infrelb ( ( ran ran 𝑔 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ran 𝑔 𝑥𝑦 ∧ ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ran ran 𝑔 ) → inf ( ran ran 𝑔 , ℝ , < ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) )
218 200 210 216 217 syl3anc ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → inf ( ran ran 𝑔 , ℝ , < ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) )
219 218 adantll ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ 𝑏𝑠 ) → inf ( ran ran 𝑔 , ℝ , < ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) )
220 219 ad2ant2r ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → inf ( ran ran 𝑔 , ℝ , < ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) )
221 1 ad3antrrr ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
222 xmetcl ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥𝑋𝑤𝑋 ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ* )
223 222 3expb ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ* )
224 221 223 sylan ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ* )
225 224 adantr ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ* )
226 simplr ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) )
227 simpl ( ( 𝑏𝑠𝑥𝑏 ) → 𝑏𝑠 )
228 216 ne0d ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → ran ran 𝑔 ≠ ∅ )
229 infrecl ( ( ran ran 𝑔 ⊆ ℝ ∧ ran ran 𝑔 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ran 𝑔 𝑥𝑦 ) → inf ( ran ran 𝑔 , ℝ , < ) ∈ ℝ )
230 200 228 210 229 syl3anc ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → inf ( ran ran 𝑔 , ℝ , < ) ∈ ℝ )
231 230 rexrd ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → inf ( ran ran 𝑔 , ℝ , < ) ∈ ℝ* )
232 226 227 231 syl2an ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → inf ( ran ran 𝑔 , ℝ , < ) ∈ ℝ* )
233 simpr ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) )
234 233 ffvelrnda ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ 𝑏𝑠 ) → ( 𝑔𝑏 ) ∈ ( 𝑋 × ℝ+ ) )
235 xp2nd ( ( 𝑔𝑏 ) ∈ ( 𝑋 × ℝ+ ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ+ )
236 234 235 syl ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ 𝑏𝑠 ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ+ )
237 236 rpxrd ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ 𝑏𝑠 ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ* )
238 237 ad2ant2r ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ* )
239 xrltletr ( ( ( 𝑥 𝐶 𝑤 ) ∈ ℝ* ∧ inf ( ran ran 𝑔 , ℝ , < ) ∈ ℝ* ∧ ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ* ) → ( ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) ∧ inf ( ran ran 𝑔 , ℝ , < ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
240 225 232 238 239 syl3anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) ∧ inf ( ran ran 𝑔 , ℝ , < ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
241 220 240 mpan2d ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
242 241 adantlr ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
243 1 ad6antr ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
244 simpllr ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) → 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) )
245 ffvelrn ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → ( 𝑔𝑏 ) ∈ ( 𝑋 × ℝ+ ) )
246 xp1st ( ( 𝑔𝑏 ) ∈ ( 𝑋 × ℝ+ ) → ( 1st ‘ ( 𝑔𝑏 ) ) ∈ 𝑋 )
247 245 246 syl ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → ( 1st ‘ ( 𝑔𝑏 ) ) ∈ 𝑋 )
248 244 227 247 syl2an ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( 1st ‘ ( 𝑔𝑏 ) ) ∈ 𝑋 )
249 simpr ( ( 𝑥𝑋𝑤𝑋 ) → 𝑤𝑋 )
250 249 ad3antlr ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → 𝑤𝑋 )
251 xmetcl ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1st ‘ ( 𝑔𝑏 ) ) ∈ 𝑋𝑤𝑋 ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) ∈ ℝ* )
252 243 248 250 251 syl3anc ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) ∈ ℝ* )
253 252 adantr ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) ∈ ℝ* )
254 245 235 syl ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ+ )
255 226 254 sylan ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ+ )
256 255 ad2ant2r ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ+ )
257 256 rpred ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ )
258 164 ad3antlr ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → 𝑥𝑋 )
259 xmetcl ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1st ‘ ( 𝑔𝑏 ) ) ∈ 𝑋𝑥𝑋 ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ* )
260 243 248 258 259 syl3anc ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ* )
261 254 rpxrd ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ* )
262 244 227 261 syl2an ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ* )
263 eleq2 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( 𝑥𝑏𝑥 ∈ ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) )
264 1 ad5antr ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
265 226 247 sylan ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( 1st ‘ ( 𝑔𝑏 ) ) ∈ 𝑋 )
266 255 rpxrd ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ* )
267 elbl ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1st ‘ ( 𝑔𝑏 ) ) ∈ 𝑋 ∧ ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ* ) → ( 𝑥 ∈ ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ↔ ( 𝑥𝑋 ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) )
268 264 265 266 267 syl3anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( 𝑥 ∈ ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ↔ ( 𝑥𝑋 ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) )
269 263 268 sylan9bbr ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) → ( 𝑥𝑏 ↔ ( 𝑥𝑋 ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) )
270 269 biimpd ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) → ( 𝑥𝑏 → ( 𝑥𝑋 ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) )
271 270 an32s ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ 𝑏𝑠 ) → ( 𝑥𝑏 → ( 𝑥𝑋 ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) )
272 271 impr ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( 𝑥𝑋 ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
273 272 simprd ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) )
274 260 262 273 xrltled ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) )
275 226 ffvelrnda ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( 𝑔𝑏 ) ∈ ( 𝑋 × ℝ+ ) )
276 275 246 syl ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( 1st ‘ ( 𝑔𝑏 ) ) ∈ 𝑋 )
277 simplrl ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → 𝑥𝑋 )
278 264 276 277 259 syl3anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ* )
279 xmetge0 ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1st ‘ ( 𝑔𝑏 ) ) ∈ 𝑋𝑥𝑋 ) → 0 ≤ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) )
280 264 276 277 279 syl3anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → 0 ≤ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) )
281 xrrege0 ( ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ* ∧ ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ ) ∧ ( 0 ≤ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ )
282 281 an4s ( ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ) ∧ ( ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ )
283 282 ex ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ) → ( ( ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ ) )
284 278 280 283 syl2anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ ) )
285 284 ad2ant2r ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ ) )
286 257 274 285 mp2and ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ )
287 286 adantr ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ )
288 xrltle ( ( ( 𝑥 𝐶 𝑤 ) ∈ ℝ* ∧ ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ* ) → ( ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) → ( 𝑥 𝐶 𝑤 ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
289 225 238 288 syl2anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) → ( 𝑥 𝐶 𝑤 ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
290 xmetge0 ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥𝑋𝑤𝑋 ) → 0 ≤ ( 𝑥 𝐶 𝑤 ) )
291 290 3expb ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → 0 ≤ ( 𝑥 𝐶 𝑤 ) )
292 221 291 sylan ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → 0 ≤ ( 𝑥 𝐶 𝑤 ) )
293 292 adantr ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → 0 ≤ ( 𝑥 𝐶 𝑤 ) )
294 236 rpred ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ 𝑏𝑠 ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ )
295 294 ad2ant2r ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ )
296 xrrege0 ( ( ( ( 𝑥 𝐶 𝑤 ) ∈ ℝ* ∧ ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ ) ∧ ( 0 ≤ ( 𝑥 𝐶 𝑤 ) ∧ ( 𝑥 𝐶 𝑤 ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ )
297 296 ex ( ( ( 𝑥 𝐶 𝑤 ) ∈ ℝ* ∧ ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ ) → ( ( 0 ≤ ( 𝑥 𝐶 𝑤 ) ∧ ( 𝑥 𝐶 𝑤 ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ ) )
298 225 295 297 syl2anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 0 ≤ ( 𝑥 𝐶 𝑤 ) ∧ ( 𝑥 𝐶 𝑤 ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ ) )
299 293 298 mpand ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 𝑥 𝐶 𝑤 ) ≤ ( 2nd ‘ ( 𝑔𝑏 ) ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ ) )
300 289 299 syld ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ ) )
301 300 adantlr ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ ) )
302 301 imp ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ )
303 287 302 readdcld ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) + ( 𝑥 𝐶 𝑤 ) ) ∈ ℝ )
304 303 rexrd ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) + ( 𝑥 𝐶 𝑤 ) ) ∈ ℝ* )
305 256 256 rpaddcld ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∈ ℝ+ )
306 305 rpxrd ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∈ ℝ* )
307 306 adantr ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∈ ℝ* )
308 xmettri ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) ∈ 𝑋𝑤𝑋𝑥𝑋 ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) ≤ ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) +𝑒 ( 𝑥 𝐶 𝑤 ) ) )
309 243 248 250 258 308 syl13anc ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) ≤ ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) +𝑒 ( 𝑥 𝐶 𝑤 ) ) )
310 309 adantr ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) ≤ ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) +𝑒 ( 𝑥 𝐶 𝑤 ) ) )
311 rexadd ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) ∈ ℝ ∧ ( 𝑥 𝐶 𝑤 ) ∈ ℝ ) → ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) +𝑒 ( 𝑥 𝐶 𝑤 ) ) = ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) + ( 𝑥 𝐶 𝑤 ) ) )
312 287 302 311 syl2anc ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) +𝑒 ( 𝑥 𝐶 𝑤 ) ) = ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) + ( 𝑥 𝐶 𝑤 ) ) )
313 310 312 breqtrd ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) ≤ ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) + ( 𝑥 𝐶 𝑤 ) ) )
314 257 adantr ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ )
315 273 adantr ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) )
316 simpr ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) )
317 287 302 314 314 315 316 lt2addd ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) + ( 𝑥 𝐶 𝑤 ) ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
318 253 304 307 313 317 xrlelttrd ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
319 318 ex ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) )
320 254 rpred ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → ( 2nd ‘ ( 𝑔𝑏 ) ) ∈ ℝ )
321 320 254 ltaddrpd ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ 𝑏𝑠 ) → ( 2nd ‘ ( 𝑔𝑏 ) ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
322 244 227 321 syl2an ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( 2nd ‘ ( 𝑔𝑏 ) ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
323 260 262 306 273 322 xrlttrd ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) )
324 319 323 jctild ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 𝑥 𝐶 𝑤 ) < ( 2nd ‘ ( 𝑔𝑏 ) ) → ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ) )
325 242 324 syld ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ) )
326 simpll ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → ( 𝜑𝑓 : 𝑋𝑌 ) )
327 ffvelrn ( ( 𝑓 : 𝑋𝑌𝑥𝑋 ) → ( 𝑓𝑥 ) ∈ 𝑌 )
328 ffvelrn ( ( 𝑓 : 𝑋𝑌𝑤𝑋 ) → ( 𝑓𝑤 ) ∈ 𝑌 )
329 327 328 anim12dan ( ( 𝑓 : 𝑋𝑌 ∧ ( 𝑥𝑋𝑤𝑋 ) ) → ( ( 𝑓𝑥 ) ∈ 𝑌 ∧ ( 𝑓𝑤 ) ∈ 𝑌 ) )
330 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝑓𝑥 ) ∈ 𝑌 ∧ ( 𝑓𝑤 ) ∈ 𝑌 ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ* )
331 330 3expb ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑌 ∧ ( 𝑓𝑤 ) ∈ 𝑌 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ* )
332 2 329 331 syl2an ( ( 𝜑 ∧ ( 𝑓 : 𝑋𝑌 ∧ ( 𝑥𝑋𝑤𝑋 ) ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ* )
333 332 anassrs ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ* )
334 326 333 sylan ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ* )
335 334 ad3antrrr ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ* )
336 2 ad5antr ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
337 simp-5r ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → 𝑓 : 𝑋𝑌 )
338 337 276 ffvelrnd ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ∈ 𝑌 )
339 simpllr ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) → 𝑓 : 𝑋𝑌 )
340 339 ffvelrnda ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ 𝑥𝑋 ) → ( 𝑓𝑥 ) ∈ 𝑌 )
341 340 adantrr ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → ( 𝑓𝑥 ) ∈ 𝑌 )
342 341 adantr ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( 𝑓𝑥 ) ∈ 𝑌 )
343 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ∈ 𝑌 ∧ ( 𝑓𝑥 ) ∈ 𝑌 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ* )
344 336 338 342 343 syl3anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ* )
345 14 rpxrd ( 𝑑 ∈ ℝ+ → ( 𝑑 / 2 ) ∈ ℝ* )
346 345 ad4antlr ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( 𝑑 / 2 ) ∈ ℝ* )
347 xrltle ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ* ∧ ( 𝑑 / 2 ) ∈ ℝ* ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ≤ ( 𝑑 / 2 ) ) )
348 344 346 347 syl2anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ≤ ( 𝑑 / 2 ) ) )
349 xmetge0 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ∈ 𝑌 ∧ ( 𝑓𝑥 ) ∈ 𝑌 ) → 0 ≤ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) )
350 336 338 342 349 syl3anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → 0 ≤ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) )
351 14 rpred ( 𝑑 ∈ ℝ+ → ( 𝑑 / 2 ) ∈ ℝ )
352 351 ad4antlr ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( 𝑑 / 2 ) ∈ ℝ )
353 xrrege0 ( ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ* ∧ ( 𝑑 / 2 ) ∈ ℝ ) ∧ ( 0 ≤ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ≤ ( 𝑑 / 2 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ )
354 353 ex ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ* ∧ ( 𝑑 / 2 ) ∈ ℝ ) → ( ( 0 ≤ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ≤ ( 𝑑 / 2 ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ ) )
355 344 352 354 syl2anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( 0 ≤ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ≤ ( 𝑑 / 2 ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ ) )
356 350 355 mpand ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ≤ ( 𝑑 / 2 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ ) )
357 348 356 syld ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ ) )
358 357 ad2ant2r ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ ) )
359 358 imp ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ )
360 339 ffvelrnda ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ 𝑤𝑋 ) → ( 𝑓𝑤 ) ∈ 𝑌 )
361 360 adantrl ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → ( 𝑓𝑤 ) ∈ 𝑌 )
362 361 adantr ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( 𝑓𝑤 ) ∈ 𝑌 )
363 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ∈ 𝑌 ∧ ( 𝑓𝑤 ) ∈ 𝑌 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ* )
364 336 338 362 363 syl3anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ* )
365 xrltle ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ* ∧ ( 𝑑 / 2 ) ∈ ℝ* ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ≤ ( 𝑑 / 2 ) ) )
366 364 346 365 syl2anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ≤ ( 𝑑 / 2 ) ) )
367 xmetge0 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ∈ 𝑌 ∧ ( 𝑓𝑤 ) ∈ 𝑌 ) → 0 ≤ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) )
368 336 338 362 367 syl3anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → 0 ≤ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) )
369 xrrege0 ( ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ* ∧ ( 𝑑 / 2 ) ∈ ℝ ) ∧ ( 0 ≤ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ≤ ( 𝑑 / 2 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ )
370 369 ex ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ* ∧ ( 𝑑 / 2 ) ∈ ℝ ) → ( ( 0 ≤ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ≤ ( 𝑑 / 2 ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ ) )
371 364 352 370 syl2anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( 0 ≤ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ≤ ( 𝑑 / 2 ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ ) )
372 368 371 mpand ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ≤ ( 𝑑 / 2 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ ) )
373 366 372 syld ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ ) )
374 373 ad2ant2r ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ ) )
375 374 imp ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ )
376 readdcl ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) ∈ ℝ )
377 359 375 376 syl2an ( ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ) ∧ ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) ∈ ℝ )
378 377 anandis ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) ∈ ℝ )
379 378 rexrd ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) ∈ ℝ* )
380 rpxr ( 𝑑 ∈ ℝ+𝑑 ∈ ℝ* )
381 380 ad6antlr ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → 𝑑 ∈ ℝ* )
382 xmettri ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( ( 𝑓𝑥 ) ∈ 𝑌 ∧ ( 𝑓𝑤 ) ∈ 𝑌 ∧ ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ∈ 𝑌 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) ≤ ( ( ( 𝑓𝑥 ) 𝐷 ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ) +𝑒 ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) )
383 336 342 362 338 382 syl13anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) ≤ ( ( ( 𝑓𝑥 ) 𝐷 ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ) +𝑒 ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) )
384 383 ad2ant2r ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) ≤ ( ( ( 𝑓𝑥 ) 𝐷 ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ) +𝑒 ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) )
385 384 adantr ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) ≤ ( ( ( 𝑓𝑥 ) 𝐷 ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ) +𝑒 ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) )
386 xmetsym ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝑓𝑥 ) ∈ 𝑌 ∧ ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ∈ 𝑌 ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ) = ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) )
387 336 342 338 386 syl3anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ) = ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) )
388 387 ad2ant2r ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ) = ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) )
389 388 adantr ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ) = ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) )
390 389 oveq1d ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( 𝑓𝑥 ) 𝐷 ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ) +𝑒 ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) = ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) +𝑒 ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) )
391 rexadd ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) +𝑒 ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) = ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) )
392 359 375 391 syl2an ( ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ) ∧ ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) +𝑒 ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) = ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) )
393 392 anandis ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) +𝑒 ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) = ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) )
394 390 393 eqtrd ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( 𝑓𝑥 ) 𝐷 ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) ) +𝑒 ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) = ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) )
395 385 394 breqtrd ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) ≤ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) )
396 lt2add ( ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ ) ∧ ( ( 𝑑 / 2 ) ∈ ℝ ∧ ( 𝑑 / 2 ) ∈ ℝ ) ) → ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) < ( ( 𝑑 / 2 ) + ( 𝑑 / 2 ) ) ) )
397 396 expcom ( ( ( 𝑑 / 2 ) ∈ ℝ ∧ ( 𝑑 / 2 ) ∈ ℝ ) → ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ ) → ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) < ( ( 𝑑 / 2 ) + ( 𝑑 / 2 ) ) ) ) )
398 352 352 397 syl2anc ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) ∈ ℝ ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ∈ ℝ ) → ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) < ( ( 𝑑 / 2 ) + ( 𝑑 / 2 ) ) ) ) )
399 357 373 398 syl2and ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) → ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) < ( ( 𝑑 / 2 ) + ( 𝑑 / 2 ) ) ) ) )
400 399 pm2.43d ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏𝑠 ) → ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) < ( ( 𝑑 / 2 ) + ( 𝑑 / 2 ) ) ) )
401 400 ad2ant2r ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) < ( ( 𝑑 / 2 ) + ( 𝑑 / 2 ) ) ) )
402 401 imp ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) < ( ( 𝑑 / 2 ) + ( 𝑑 / 2 ) ) )
403 rpcn ( 𝑑 ∈ ℝ+𝑑 ∈ ℂ )
404 403 2halvesd ( 𝑑 ∈ ℝ+ → ( ( 𝑑 / 2 ) + ( 𝑑 / 2 ) ) = 𝑑 )
405 404 ad6antlr ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( 𝑑 / 2 ) + ( 𝑑 / 2 ) ) = 𝑑 )
406 402 405 breqtrd ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) + ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) ) < 𝑑 )
407 335 379 381 395 406 xrlelttrd ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) ∧ ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 )
408 407 ex ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) )
409 325 408 imim12d ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
410 198 409 sylanl1 ( ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
411 410 adantlrr ( ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑥 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑤 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) ) → ( ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑥 ) ) < ( 𝑑 / 2 ) ∧ ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) ) → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
412 195 411 mpd ( ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ∧ ( 𝑏𝑠𝑥𝑏 ) ) → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) )
413 412 exp32 ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) → ( 𝑏𝑠 → ( 𝑥𝑏 → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) ) )
414 176 413 sylan2 ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ( ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ∧ 𝑏𝑠 ) ) → ( 𝑏𝑠 → ( 𝑥𝑏 → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) ) )
415 414 expr ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) → ( 𝑏𝑠 → ( 𝑏𝑠 → ( 𝑥𝑏 → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) ) ) )
416 415 pm2.43d ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) → ( 𝑏𝑠 → ( 𝑥𝑏 → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) ) )
417 416 an32s ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → ( 𝑏𝑠 → ( 𝑥𝑏 → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) ) )
418 174 175 417 rexlimd ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → ( ∃ 𝑏𝑠 𝑥𝑏 → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
419 169 418 mpd ( ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ∧ ( 𝑥𝑋𝑤𝑋 ) ) → ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) )
420 419 ralrimivva ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) → ∀ 𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) )
421 breq2 ( 𝑧 = inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑥 𝐶 𝑤 ) < 𝑧 ↔ ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) ) )
422 421 imbi1d ( 𝑧 = inf ( ran ran 𝑔 , ℝ , < ) → ( ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ↔ ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
423 422 2ralbidv ( 𝑧 = inf ( ran ran 𝑔 , ℝ , < ) → ( ∀ 𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ↔ ∀ 𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
424 423 rspcev ( ( inf ( ran ran 𝑔 , ℝ , < ) ∈ ℝ+ ∧ ∀ 𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < inf ( ran ran 𝑔 , ℝ , < ) → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) → ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) )
425 160 420 424 syl2anc ( ( ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) ∧ 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) → ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) )
426 425 expl ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) → ( ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) → ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
427 426 exlimdv ( ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) ∧ ( MetOpen ‘ 𝐶 ) = 𝑠 ) → ( ∃ 𝑔 ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) → ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
428 427 expimpd ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ Fin ) → ( ( ( MetOpen ‘ 𝐶 ) = 𝑠 ∧ ∃ 𝑔 ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ) → ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
429 105 428 sylan2 ( ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑠 ∈ ( 𝒫 ( MetOpen ‘ 𝐶 ) ∩ Fin ) ) → ( ( ( MetOpen ‘ 𝐶 ) = 𝑠 ∧ ∃ 𝑔 ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ) → ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
430 429 rexlimdva ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) → ( ∃ 𝑠 ∈ ( 𝒫 ( MetOpen ‘ 𝐶 ) ∩ Fin ) ( ( MetOpen ‘ 𝐶 ) = 𝑠 ∧ ∃ 𝑔 ( 𝑔 : 𝑠 ⟶ ( 𝑋 × ℝ+ ) ∧ ∀ 𝑏𝑠 ( 𝑏 = ( ( 1st ‘ ( 𝑔𝑏 ) ) ( ball ‘ 𝐶 ) ( 2nd ‘ ( 𝑔𝑏 ) ) ) ∧ ∀ 𝑐𝑋 ( ( ( 1st ‘ ( 𝑔𝑏 ) ) 𝐶 𝑐 ) < ( ( 2nd ‘ ( 𝑔𝑏 ) ) + ( 2nd ‘ ( 𝑔𝑏 ) ) ) → ( ( 𝑓 ‘ ( 1st ‘ ( 𝑔𝑏 ) ) ) 𝐷 ( 𝑓𝑐 ) ) < ( 𝑑 / 2 ) ) ) ) ) → ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
431 104 430 syld ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) → ( ∀ 𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < ( 𝑑 / 2 ) ) → ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
432 20 431 syl5 ( ( ( 𝜑𝑓 : 𝑋𝑌 ) ∧ 𝑑 ∈ ℝ+ ) → ( ( ( 𝑑 / 2 ) ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
433 432 exp4b ( ( 𝜑𝑓 : 𝑋𝑌 ) → ( 𝑑 ∈ ℝ+ → ( ( 𝑑 / 2 ) ∈ ℝ+ → ( ∀ 𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) → ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) ) ) )
434 14 433 mpdi ( ( 𝜑𝑓 : 𝑋𝑌 ) → ( 𝑑 ∈ ℝ+ → ( ∀ 𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) → ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) ) )
435 434 ralrimiv ( ( 𝜑𝑓 : 𝑋𝑌 ) → ∀ 𝑑 ∈ ℝ+ ( ∀ 𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) → ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
436 r19.21v ( ∀ 𝑑 ∈ ℝ+ ( ∀ 𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) → ∃ 𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) ↔ ( ∀ 𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) → ∀ 𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
437 435 436 sylib ( ( 𝜑𝑓 : 𝑋𝑌 ) → ( ∀ 𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) → ∀ 𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) )
438 13 437 impbid2 ( ( 𝜑𝑓 : 𝑋𝑌 ) → ( ∀ 𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ↔ ∀ 𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ) )
439 ralcom ( ∀ 𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) )
440 438 439 bitrdi ( ( 𝜑𝑓 : 𝑋𝑌 ) → ( ∀ 𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ↔ ∀ 𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ) )
441 440 pm5.32da ( 𝜑 → ( ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) ↔ ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ) ) )
442 eqid ( metUnif ‘ 𝐶 ) = ( metUnif ‘ 𝐶 )
443 eqid ( metUnif ‘ 𝐷 ) = ( metUnif ‘ 𝐷 )
444 xmetpsmet ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → 𝐶 ∈ ( PsMet ‘ 𝑋 ) )
445 1 444 syl ( 𝜑𝐶 ∈ ( PsMet ‘ 𝑋 ) )
446 xmetpsmet ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) → 𝐷 ∈ ( PsMet ‘ 𝑌 ) )
447 2 446 syl ( 𝜑𝐷 ∈ ( PsMet ‘ 𝑌 ) )
448 442 443 4 5 445 447 metucn ( 𝜑 → ( 𝑓 ∈ ( ( metUnif ‘ 𝐶 ) Cnu ( metUnif ‘ 𝐷 ) ) ↔ ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑑 ) ) ) )
449 eqid ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
450 26 449 metcn ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝑓 ∈ ( ( MetOpen ‘ 𝐶 ) Cn ( MetOpen ‘ 𝐷 ) ) ↔ ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ) ) )
451 1 2 450 syl2anc ( 𝜑 → ( 𝑓 ∈ ( ( MetOpen ‘ 𝐶 ) Cn ( MetOpen ‘ 𝐷 ) ) ↔ ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑓𝑥 ) 𝐷 ( 𝑓𝑤 ) ) < 𝑦 ) ) ) )
452 441 448 451 3bitr4d ( 𝜑 → ( 𝑓 ∈ ( ( metUnif ‘ 𝐶 ) Cnu ( metUnif ‘ 𝐷 ) ) ↔ 𝑓 ∈ ( ( MetOpen ‘ 𝐶 ) Cn ( MetOpen ‘ 𝐷 ) ) ) )
453 452 eqrdv ( 𝜑 → ( ( metUnif ‘ 𝐶 ) Cnu ( metUnif ‘ 𝐷 ) ) = ( ( MetOpen ‘ 𝐶 ) Cn ( MetOpen ‘ 𝐷 ) ) )