Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heicant Structured version   Visualization version   GIF version

Theorem heicant 37990
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.)
Hypotheses
Ref Expression
heicant.c (𝜑𝐶 ∈ (∞Met‘𝑋))
heicant.d (𝜑𝐷 ∈ (∞Met‘𝑌))
heicant.j (𝜑 → (MetOpen‘𝐶) ∈ Comp)
heicant.x (𝜑𝑋 ≠ ∅)
heicant.y (𝜑𝑌 ≠ ∅)
Assertion
Ref Expression
heicant (𝜑 → ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) = ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)))

Proof of Theorem heicant
Dummy variables 𝑏 𝑐 𝑑 𝑓 𝑔 𝑝 𝑠 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 5090 . . . . . . . . . . 11 (𝑑 = 𝑦 → (((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑 ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
21imbi2d 340 . . . . . . . . . 10 (𝑑 = 𝑦 → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
322ralbidv 3202 . . . . . . . . 9 (𝑑 = 𝑦 → (∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
43rexbidv 3162 . . . . . . . 8 (𝑑 = 𝑦 → (∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
54cbvralvw 3216 . . . . . . 7 (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
6 r19.12 3287 . . . . . . . 8 (∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
76ralimi 3075 . . . . . . 7 (∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
85, 7sylbi 217 . . . . . 6 (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) → ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
9 rphalfcl 12962 . . . . . . . . 9 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ+)
10 breq2 5090 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑑 / 2) → (((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦 ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
1110imbi2d 340 . . . . . . . . . . . . . . 15 (𝑦 = (𝑑 / 2) → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1211ralbidv 3161 . . . . . . . . . . . . . 14 (𝑦 = (𝑑 / 2) → (∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1312rexbidv 3162 . . . . . . . . . . . . 13 (𝑦 = (𝑑 / 2) → (∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1413ralbidv 3161 . . . . . . . . . . . 12 (𝑦 = (𝑑 / 2) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1514rspcva 3563 . . . . . . . . . . 11 (((𝑑 / 2) ∈ ℝ+ ∧ ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)) → ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
16 heicant.j . . . . . . . . . . . . . . 15 (𝜑 → (MetOpen‘𝐶) ∈ Comp)
1716ad3antrrr 731 . . . . . . . . . . . . . 14 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (MetOpen‘𝐶) ∈ Comp)
18 heicant.c . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐶 ∈ (∞Met‘𝑋))
1918ad2antrr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → 𝐶 ∈ (∞Met‘𝑋))
2019anim1i 616 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) → (𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋))
21 rphalfcl 12962 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → (𝑧 / 2) ∈ ℝ+)
2221rpxrd 12978 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ℝ+ → (𝑧 / 2) ∈ ℝ*)
23 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . 23 (MetOpen‘𝐶) = (MetOpen‘𝐶)
2423blopn 24475 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋 ∧ (𝑧 / 2) ∈ ℝ*) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
25243expa 1119 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧 / 2) ∈ ℝ*) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2620, 22, 25syl2an 597 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2726adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2821rpgt0d 12980 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → 0 < (𝑧 / 2))
2922, 28jca 511 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ℝ+ → ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2)))
30 xblcntr 24386 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋 ∧ ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
31303expa 1119 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
3220, 29, 31syl2an 597 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
3332adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
34 opelxpi 5661 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑋 ∧ (𝑧 / 2) ∈ ℝ+) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
3521, 34sylan2 594 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑋𝑧 ∈ ℝ+) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
3635ad4ant23 754 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
37 rpcn 12944 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ ℝ+𝑧 ∈ ℂ)
38372halvesd 12414 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℝ+ → ((𝑧 / 2) + (𝑧 / 2)) = 𝑧)
3938breq2d 5098 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ℝ+ → ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) ↔ (𝑥𝐶𝑐) < 𝑧))
4039imbi1d 341 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ℝ+ → (((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
4140ralbidv 3161 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ ℝ+ → (∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
42 oveq2 7368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑤 → (𝑥𝐶𝑐) = (𝑥𝐶𝑤))
4342breq1d 5096 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑤 → ((𝑥𝐶𝑐) < 𝑧 ↔ (𝑥𝐶𝑤) < 𝑧))
44 fveq2 6834 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 = 𝑤 → (𝑓𝑐) = (𝑓𝑤))
4544oveq2d 7376 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑤 → ((𝑓𝑥)𝐷(𝑓𝑐)) = ((𝑓𝑥)𝐷(𝑓𝑤)))
4645breq1d 5096 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑤 → (((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
4743, 46imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑤 → (((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
4847cbvralvw 3216 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐𝑋 ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
4941, 48bitrdi 287 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → (∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
5049biimpar 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 ∈ ℝ+ ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
5150adantll 715 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
52 vex 3434 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥 ∈ V
53 ovex 7393 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 / 2) ∈ V
5452, 53op1std 7945 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (1st𝑝) = 𝑥)
5552, 53op2ndd 7946 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (2nd𝑝) = (𝑧 / 2))
5654, 55oveq12d 7378 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((1st𝑝)(ball‘𝐶)(2nd𝑝)) = (𝑥(ball‘𝐶)(𝑧 / 2)))
5756eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)))
5857biantrurd 532 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
5954oveq1d 7375 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((1st𝑝)𝐶𝑐) = (𝑥𝐶𝑐))
6055, 55oveq12d 7378 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((2nd𝑝) + (2nd𝑝)) = ((𝑧 / 2) + (𝑧 / 2)))
6159, 60breq12d 5099 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) ↔ (𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2))))
6254fveq2d 6838 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (𝑓‘(1st𝑝)) = (𝑓𝑥))
6362oveq1d 7375 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) = ((𝑓𝑥)𝐷(𝑓𝑐)))
6463breq1d 5096 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
6561, 64imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
6665ralbidv 3161 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
6758, 66bitr3d 281 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
6867rspcev 3565 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+) ∧ ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))) → ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))
6936, 51, 68syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))
70 eleq2 2826 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (𝑥𝑏𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2))))
71 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ↔ (𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝))))
7271anbi1d 632 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → ((𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7372rexbidv 3162 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7470, 73anbi12d 633 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → ((𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ (𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)) ∧ ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
7574rspcev 3565 . . . . . . . . . . . . . . . . . . 19 (((𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶) ∧ (𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)) ∧ ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7627, 33, 69, 75syl12anc 837 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7776rexlimdva2 3141 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) → (∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
7877ralimdva 3150 . . . . . . . . . . . . . . . 16 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
7978imp 406 . . . . . . . . . . . . . . 15 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
8023mopnuni 24416 . . . . . . . . . . . . . . . . . 18 (𝐶 ∈ (∞Met‘𝑋) → 𝑋 = (MetOpen‘𝐶))
8118, 80syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 = (MetOpen‘𝐶))
8281raleqdv 3296 . . . . . . . . . . . . . . . 16 (𝜑 → (∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
8382ad3antrrr 731 . . . . . . . . . . . . . . 15 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
8479, 83mpbid 232 . . . . . . . . . . . . . 14 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
85 eqid 2737 . . . . . . . . . . . . . . 15 (MetOpen‘𝐶) = (MetOpen‘𝐶)
86 fveq2 6834 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (1st𝑝) = (1st ‘(𝑔𝑏)))
87 fveq2 6834 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (2nd𝑝) = (2nd ‘(𝑔𝑏)))
8886, 87oveq12d 7378 . . . . . . . . . . . . . . . . 17 (𝑝 = (𝑔𝑏) → ((1st𝑝)(ball‘𝐶)(2nd𝑝)) = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))))
8988eqeq2d 2748 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑔𝑏) → (𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ↔ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))))
9086oveq1d 7375 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((1st𝑝)𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑐))
9187, 87oveq12d 7378 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((2nd𝑝) + (2nd𝑝)) = ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
9290, 91breq12d 5099 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) ↔ ((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
9386fveq2d 6838 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = (𝑔𝑏) → (𝑓‘(1st𝑝)) = (𝑓‘(1st ‘(𝑔𝑏))))
9493oveq1d 7375 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)))
9594breq1d 5096 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))
9692, 95imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑝 = (𝑔𝑏) → ((((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
9796ralbidv 3161 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑔𝑏) → (∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
9889, 97anbi12d 633 . . . . . . . . . . . . . . 15 (𝑝 = (𝑔𝑏) → ((𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
9985, 98cmpcovf 23366 . . . . . . . . . . . . . 14 (((MetOpen‘𝐶) ∈ Comp ∧ ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
10017, 84, 99syl2anc 585 . . . . . . . . . . . . 13 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
101100ex 412 . . . . . . . . . . . 12 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))))))
102 elinel2 4143 . . . . . . . . . . . . . 14 (𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin) → 𝑠 ∈ Fin)
103 simpll 767 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → 𝜑)
104103anim1i 616 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → (𝜑𝑠 ∈ Fin))
105 frn 6669 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran 𝑔 ⊆ (𝑋 × ℝ+))
106 rnss 5888 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ⊆ (𝑋 × ℝ+) → ran ran 𝑔 ⊆ ran (𝑋 × ℝ+))
107105, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ran (𝑋 × ℝ+))
108 rnxpss 6130 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑋 × ℝ+) ⊆ ℝ+
109107, 108sstrdi 3935 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ℝ+)
110109adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ⊆ ℝ+)
111 simplr 769 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → 𝑠 ∈ Fin)
112 ffun 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔:𝑠⟶(𝑋 × ℝ+) → Fun 𝑔)
113 vex 3434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑔 ∈ V
114113fundmen 8971 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun 𝑔 → dom 𝑔𝑔)
115114ensymd 8945 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Fun 𝑔𝑔 ≈ dom 𝑔)
116112, 115syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔 ≈ dom 𝑔)
117 fdm 6671 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → dom 𝑔 = 𝑠)
118116, 117breqtrd 5112 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔𝑠)
119 enfii 9113 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ Fin ∧ 𝑔𝑠) → 𝑔 ∈ Fin)
120118, 119sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ Fin ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑔 ∈ Fin)
121 rnfi 9243 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 ∈ Fin → ran 𝑔 ∈ Fin)
122 rnfi 9243 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ∈ Fin → ran ran 𝑔 ∈ Fin)
123120, 121, 1223syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ Fin ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ∈ Fin)
124111, 123sylan 581 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ∈ Fin)
125117adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → dom 𝑔 = 𝑠)
126 eqtr 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → 𝑋 = 𝑠)
12781, 126sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑋 = 𝑠)
128 heicant.x . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑋 ≠ ∅)
129128adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑋 ≠ ∅)
130127, 129eqnetrrd 3001 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑠 ≠ ∅)
131 unieq 4862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑠 = ∅ → 𝑠 = ∅)
132 uni0 4879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ = ∅
133131, 132eqtrdi 2788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 = ∅ → 𝑠 = ∅)
134133necon3i 2965 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( 𝑠 ≠ ∅ → 𝑠 ≠ ∅)
135130, 134syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑠 ≠ ∅)
136135adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑠 ≠ ∅)
137125, 136eqnetrd 3000 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → dom 𝑔 ≠ ∅)
138 dm0rn0 5873 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑔 = ∅ ↔ ran 𝑔 = ∅)
139138necon3bii 2985 . . . . . . . . . . . . . . . . . . . . . . . . 25 (dom 𝑔 ≠ ∅ ↔ ran 𝑔 ≠ ∅)
140137, 139sylib 218 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran 𝑔 ≠ ∅)
141 relxp 5642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Rel (𝑋 × ℝ+)
142 relss 5731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ran 𝑔 ⊆ (𝑋 × ℝ+) → (Rel (𝑋 × ℝ+) → Rel ran 𝑔))
143105, 141, 142mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → Rel ran 𝑔)
144 relrn0 5922 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Rel ran 𝑔 → (ran 𝑔 = ∅ ↔ ran ran 𝑔 = ∅))
145144necon3bid 2977 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Rel ran 𝑔 → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
146143, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔:𝑠⟶(𝑋 × ℝ+) → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
147146adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
148140, 147mpbid 232 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ≠ ∅)
149148adantllr 720 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ≠ ∅)
150 rpssre 12941 . . . . . . . . . . . . . . . . . . . . . . 23 + ⊆ ℝ
151110, 150sstrdi 3935 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ⊆ ℝ)
152 ltso 11217 . . . . . . . . . . . . . . . . . . . . . . 23 < Or ℝ
153 fiinfcl 9409 . . . . . . . . . . . . . . . . . . . . . . 23 (( < Or ℝ ∧ (ran ran 𝑔 ∈ Fin ∧ ran ran 𝑔 ≠ ∅ ∧ ran ran 𝑔 ⊆ ℝ)) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
154152, 153mpan 691 . . . . . . . . . . . . . . . . . . . . . 22 ((ran ran 𝑔 ∈ Fin ∧ ran ran 𝑔 ≠ ∅ ∧ ran ran 𝑔 ⊆ ℝ) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
155124, 149, 151, 154syl3anc 1374 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
156110, 155sseldd 3923 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
157104, 156sylanl1 681 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
158157adantr 480 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
15981ad3antrrr 731 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → 𝑋 = (MetOpen‘𝐶))
160159anim1i 616 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠))
161160ad2antrr 727 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠))
162 simpl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑋𝑤𝑋) → 𝑥𝑋)
163126eleq2d 2823 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑥𝑋𝑥 𝑠))
164 eluni2 4855 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 𝑠 ↔ ∃𝑏𝑠 𝑥𝑏)
165163, 164bitrdi 287 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑥𝑋 ↔ ∃𝑏𝑠 𝑥𝑏))
166165biimpa 476 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑥𝑋) → ∃𝑏𝑠 𝑥𝑏)
167161, 162, 166syl2an 597 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋)) → ∃𝑏𝑠 𝑥𝑏)
168 nfv 1916 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏(((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+))
169 nfra1 3262 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))
170168, 169nfan 1901 . . . . . . . . . . . . . . . . . . . . . 22 𝑏((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
171 nfv 1916 . . . . . . . . . . . . . . . . . . . . . 22 𝑏(𝑥𝑋𝑤𝑋)
172170, 171nfan 1901 . . . . . . . . . . . . . . . . . . . . 21 𝑏(((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋))
173 nfv 1916 . . . . . . . . . . . . . . . . . . . . 21 𝑏((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)
174 rspa 3227 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ 𝑏𝑠) → (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
175 oveq2 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑥 → ((1st ‘(𝑔𝑏))𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑥))
176175breq1d 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑥 → (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ↔ ((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
177 fveq2 6834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑐 = 𝑥 → (𝑓𝑐) = (𝑓𝑥))
178177oveq2d 7376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑥 → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
179178breq1d 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑥 → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)))
180176, 179imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑥 → ((((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2))))
181180rspcva 3563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑥𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)))
182 oveq2 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑤 → ((1st ‘(𝑔𝑏))𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑤))
183182breq1d 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ↔ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
18444oveq2d 7376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑤 → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
185184breq1d 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)))
186183, 185imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑤 → ((((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
187186rspcva 3563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑤𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)))
188181, 187anim12i 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑥𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ (𝑤𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
189188anandirs 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥𝑋𝑤𝑋) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
190 anim12 809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
191189, 190syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥𝑋𝑤𝑋) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
192191adantrl 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥𝑋𝑤𝑋) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
193192ad4ant23 754 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑏𝑠𝑥𝑏)) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
194 simpll 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → ((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+))
195194anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)))
196195anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)))
197109, 150sstrdi 3935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ℝ)
198197adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ran ran 𝑔 ⊆ ℝ)
199 0re 11137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 ∈ ℝ
200 rpge0 12947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 ∈ ℝ+ → 0 ≤ 𝑦)
201200rgen 3054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 𝑦 ∈ ℝ+ 0 ≤ 𝑦
202 ssralv 3991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (ran ran 𝑔 ⊆ ℝ+ → (∀𝑦 ∈ ℝ+ 0 ≤ 𝑦 → ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦))
203109, 201, 202mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔:𝑠⟶(𝑋 × ℝ+) → ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦)
204 breq1 5089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑥 = 0 → (𝑥𝑦 ↔ 0 ≤ 𝑦))
205204ralbidv 3161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑥 = 0 → (∀𝑦 ∈ ran ran 𝑔 𝑥𝑦 ↔ ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦))
206205rspcev 3565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((0 ∈ ℝ ∧ ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
207199, 203, 206sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑔:𝑠⟶(𝑋 × ℝ+) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
208207adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
209143adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → Rel ran 𝑔)
210 ffn 6662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔 Fn 𝑠)
211 fnfvelrn 7026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔 Fn 𝑠𝑏𝑠) → (𝑔𝑏) ∈ ran 𝑔)
212210, 211sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ ran 𝑔)
213 2ndrn 7987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((Rel ran 𝑔 ∧ (𝑔𝑏) ∈ ran 𝑔) → (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔)
214209, 212, 213syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔)
215 infrelb 12132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((ran ran 𝑔 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦 ∧ (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
216198, 208, 214, 215syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
217216adantll 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
218217ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
21918ad3antrrr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝐶 ∈ (∞Met‘𝑋))
220 xmetcl 24306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋𝑤𝑋) → (𝑥𝐶𝑤) ∈ ℝ*)
2212203expb 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥𝑋𝑤𝑋)) → (𝑥𝐶𝑤) ∈ ℝ*)
222219, 221sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑥𝐶𝑤) ∈ ℝ*)
223222adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (𝑥𝐶𝑤) ∈ ℝ*)
224 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → 𝑔:𝑠⟶(𝑋 × ℝ+))
225 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑏𝑠𝑥𝑏) → 𝑏𝑠)
226214ne0d 4283 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ran ran 𝑔 ≠ ∅)
227 infrecl 12129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((ran ran 𝑔 ⊆ ℝ ∧ ran ran 𝑔 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ)
228198, 226, 208, 227syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ)
229228rexrd 11186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ*)
230224, 225, 229syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ*)
231 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑔:𝑠⟶(𝑋 × ℝ+))
232231ffvelcdmda 7030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
233 xp2nd 7968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔𝑏) ∈ (𝑋 × ℝ+) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
234232, 233syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
235234rpxrd 12978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
236235ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
237 xrltletr 13099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑥𝐶𝑤) ∈ ℝ* ∧ inf(ran ran 𝑔, ℝ, < ) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → (((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) ∧ inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
238223, 230, 236, 237syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) ∧ inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
239218, 238mpan2d 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
240239adantlr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
24118ad6antr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝐶 ∈ (∞Met‘𝑋))
242 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → 𝑔:𝑠⟶(𝑋 × ℝ+))
243 ffvelcdm 7027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
244 xp1st 7967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔𝑏) ∈ (𝑋 × ℝ+) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
245243, 244syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
246242, 225, 245syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
247 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑥𝑋𝑤𝑋) → 𝑤𝑋)
248247ad3antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝑤𝑋)
249 xmetcl 24306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑤𝑋) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
250241, 246, 248, 249syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
251250adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
252243, 233syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
253224, 252sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
254253ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
255254rpred 12977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
256162ad3antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝑥𝑋)
257 xmetcl 24306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑥𝑋) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
258241, 246, 256, 257syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
259252rpxrd 12978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
260242, 225, 259syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
261 eleq2 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) → (𝑥𝑏𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))))
26218ad5antr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝐶 ∈ (∞Met‘𝑋))
263224, 245sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
264253rpxrd 12978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
265 elbl 24363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋 ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → (𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
266262, 263, 264, 265syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
267261, 266sylan9bbr 510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → (𝑥𝑏 ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
268267biimpd 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → (𝑥𝑏 → (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
269268an32s 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ 𝑏𝑠) → (𝑥𝑏 → (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
270269impr 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏))))
271270simprd 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))
272258, 260, 271xrltled 13092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))
273224ffvelcdmda 7030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
274273, 244syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
275 simplrl 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝑥𝑋)
276262, 274, 275, 257syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
277 xmetge0 24319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑥𝑋) → 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥))
278262, 274, 275, 277syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥))
279 xrrege0 13117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) ∧ (0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥) ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
280279an4s 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥)) ∧ ((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
281280ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥)) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
282276, 278, 281syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
283282ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
284255, 272, 283mp2and 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
285284adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
286 xrltle 13091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))))
287223, 236, 286syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))))
288 xmetge0 24319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋𝑤𝑋) → 0 ≤ (𝑥𝐶𝑤))
2892883expb 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥𝑋𝑤𝑋)) → 0 ≤ (𝑥𝐶𝑤))
290219, 289sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → 0 ≤ (𝑥𝐶𝑤))
291290adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → 0 ≤ (𝑥𝐶𝑤))
292234rpred 12977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
293292ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
294 xrrege0 13117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) ∧ (0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏)))) → (𝑥𝐶𝑤) ∈ ℝ)
295294ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) → ((0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ))
296223, 293, 295syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ))
297291, 296mpand 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
298287, 297syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
299298adantlr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
300299imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ)
301285, 300readdcld 11165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) ∈ ℝ)
302301rexrd 11186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) ∈ ℝ*)
303254, 254rpaddcld 12992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ+)
304303rpxrd 12978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ*)
305304adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ*)
306 xmettri 24326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐶 ∈ (∞Met‘𝑋) ∧ ((1st ‘(𝑔𝑏)) ∈ 𝑋𝑤𝑋𝑥𝑋)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
307241, 246, 248, 256, 306syl13anc 1375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
308307adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
309 rexadd 13175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ ∧ (𝑥𝐶𝑤) ∈ ℝ) → (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)) = (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)))
310285, 300, 309syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)) = (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)))
311308, 310breqtrd 5112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)))
312255adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
313271adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))
314 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)))
315285, 300, 312, 312, 313, 314lt2addd 11764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
316251, 302, 305, 311, 315xrlelttrd 13102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
317316ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
318252rpred 12977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
319318, 252ltaddrpd 13010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
320242, 225, 319syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
321258, 260, 304, 271, 320xrlttrd 13101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
322317, 321jctild 525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))))
323240, 322syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))))
324 simpll 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (𝜑𝑓:𝑋𝑌))
325 heicant.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑𝐷 ∈ (∞Met‘𝑌))
326 ffvelcdm 7027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑓:𝑋𝑌𝑥𝑋) → (𝑓𝑥) ∈ 𝑌)
327 ffvelcdm 7027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑓:𝑋𝑌𝑤𝑋) → (𝑓𝑤) ∈ 𝑌)
328326, 327anim12dan 620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑋𝑌 ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌))
329 xmetcl 24306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
3303293expb 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐷 ∈ (∞Met‘𝑌) ∧ ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
331325, 328, 330syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑 ∧ (𝑓:𝑋𝑌 ∧ (𝑥𝑋𝑤𝑋))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
332331anassrs 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓:𝑋𝑌) ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
333324, 332sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
334333ad3antrrr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
335325ad5antr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝐷 ∈ (∞Met‘𝑌))
336 simp-5r 786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝑓:𝑋𝑌)
337336, 274ffvelcdmd 7031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌)
338 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑓:𝑋𝑌)
339338ffvelcdmda 7030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑥𝑋) → (𝑓𝑥) ∈ 𝑌)
340339adantrr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑓𝑥) ∈ 𝑌)
341340adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓𝑥) ∈ 𝑌)
342 xmetcl 24306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑥) ∈ 𝑌) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ*)
343335, 337, 341, 342syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ*)
3449rpxrd 12978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ*)
345344ad4antlr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑑 / 2) ∈ ℝ*)
346 xrltle 13091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ*) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)))
347343, 345, 346syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)))
348 xmetge0 24319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑥) ∈ 𝑌) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
349335, 337, 341, 348syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
3509rpred 12977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ)
351350ad4antlr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑑 / 2) ∈ ℝ)
352 xrrege0 13117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) ∧ (0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ)
353352ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
354343, 351, 353syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
355349, 354mpand 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
356347, 355syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
357356ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
358357imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ)
359338ffvelcdmda 7030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑤𝑋) → (𝑓𝑤) ∈ 𝑌)
360359adantrl 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑓𝑤) ∈ 𝑌)
361360adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓𝑤) ∈ 𝑌)
362 xmetcl 24306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ*)
363335, 337, 361, 362syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ*)
364 xrltle 13091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ*) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)))
365363, 345, 364syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)))
366 xmetge0 24319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
367335, 337, 361, 366syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
368 xrrege0 13117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) ∧ (0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ)
369368ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
370363, 351, 369syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
371367, 370mpand 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
372365, 371syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
373372ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
374373imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ)
375 readdcl 11112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
376358, 374, 375syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
377376anandis 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
378377rexrd 11186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ*)
379 rpxr 12943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 ∈ ℝ+𝑑 ∈ ℝ*)
380379ad6antlr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → 𝑑 ∈ ℝ*)
381 xmettri 24326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐷 ∈ (∞Met‘𝑌) ∧ ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌 ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
382335, 341, 361, 337, 381syl13anc 1375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
383382ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
384383adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
385 xmetsym 24322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓𝑥) ∈ 𝑌 ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
386335, 341, 337, 385syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
387386ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
388387adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
389388oveq1d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
390 rexadd 13175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
391358, 374, 390syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
392391anandis 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
393389, 392eqtrd 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
394384, 393breqtrd 5112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
395 lt2add 11626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) ∧ ((𝑑 / 2) ∈ ℝ ∧ (𝑑 / 2) ∈ ℝ)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2))))
396395expcom 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑑 / 2) ∈ ℝ ∧ (𝑑 / 2) ∈ ℝ) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))))
397351, 351, 396syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))))
398356, 372, 397syl2and 609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))))
399398pm2.43d 53 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2))))
400399ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2))))
401400imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))
402 rpcn 12944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑑 ∈ ℝ+𝑑 ∈ ℂ)
4034022halvesd 12414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 ∈ ℝ+ → ((𝑑 / 2) + (𝑑 / 2)) = 𝑑)
404403ad6antlr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑑 / 2) + (𝑑 / 2)) = 𝑑)
405401, 404breqtrd 5112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < 𝑑)
406334, 378, 380, 394, 405xrlelttrd 13102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)
407406ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
408323, 407imim12d 81 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
409196, 408sylanl1 681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
410409adantlrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑏𝑠𝑥𝑏)) → (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
411193, 410mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
412411exp32 420 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
413174, 412sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ 𝑏𝑠)) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
414413expr 456 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑏𝑠 → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))))
415414pm2.43d 53 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
416415an32s 653 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋)) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
417172, 173, 416rexlimd 3245 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋)) → (∃𝑏𝑠 𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
418167, 417mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
419418ralrimivva 3181 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
420 breq2 5090 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → ((𝑥𝐶𝑤) < 𝑧 ↔ (𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < )))
421420imbi1d 341 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
4224212ralbidv 3202 . . . . . . . . . . . . . . . . . . 19 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → (∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
423422rspcev 3565 . . . . . . . . . . . . . . . . . 18 ((inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+ ∧ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
424158, 419, 423syl2anc 585 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
425424expl 457 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
426425exlimdv 1935 . . . . . . . . . . . . . . 15 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → (∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
427426expimpd 453 . . . . . . . . . . . . . 14 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → (( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
428102, 427sylan2 594 . . . . . . . . . . . . 13 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)) → (( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
429428rexlimdva 3139 . . . . . . . . . . . 12 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
430101, 429syld 47 . . . . . . . . . . 11 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
43115, 430syl5 34 . . . . . . . . . 10 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (((𝑑 / 2) ∈ ℝ+ ∧ ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
432431exp4b 430 . . . . . . . . 9 ((𝜑𝑓:𝑋𝑌) → (𝑑 ∈ ℝ+ → ((𝑑 / 2) ∈ ℝ+ → (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))))
4339, 432mpdi 45 . . . . . . . 8 ((𝜑𝑓:𝑋𝑌) → (𝑑 ∈ ℝ+ → (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
434433ralrimiv 3129 . . . . . . 7 ((𝜑𝑓:𝑋𝑌) → ∀𝑑 ∈ ℝ+ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
435 r19.21v 3163 . . . . . . 7 (∀𝑑 ∈ ℝ+ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) ↔ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
436434, 435sylib 218 . . . . . 6 ((𝜑𝑓:𝑋𝑌) → (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
4378, 436impbid2 226 . . . . 5 ((𝜑𝑓:𝑋𝑌) → (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
438 ralcom 3266 . . . . 5 (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
439437, 438bitrdi 287 . . . 4 ((𝜑𝑓:𝑋𝑌) → (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
440439pm5.32da 579 . . 3 (𝜑 → ((𝑓:𝑋𝑌 ∧ ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
441 eqid 2737 . . . 4 (metUnif‘𝐶) = (metUnif‘𝐶)
442 eqid 2737 . . . 4 (metUnif‘𝐷) = (metUnif‘𝐷)
443 heicant.y . . . 4 (𝜑𝑌 ≠ ∅)
444 xmetpsmet 24323 . . . . 5 (𝐶 ∈ (∞Met‘𝑋) → 𝐶 ∈ (PsMet‘𝑋))
44518, 444syl 17 . . . 4 (𝜑𝐶 ∈ (PsMet‘𝑋))
446 xmetpsmet 24323 . . . . 5 (𝐷 ∈ (∞Met‘𝑌) → 𝐷 ∈ (PsMet‘𝑌))
447325, 446syl 17 . . . 4 (𝜑𝐷 ∈ (PsMet‘𝑌))
448441, 442, 128, 443, 445, 447metucn 24546 . . 3 (𝜑 → (𝑓 ∈ ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
449 eqid 2737 . . . . 5 (MetOpen‘𝐷) = (MetOpen‘𝐷)
45023, 449metcn 24518 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) → (𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
45118, 325, 450syl2anc 585 . . 3 (𝜑 → (𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
452440, 448, 4513bitr4d 311 . 2 (𝜑 → (𝑓 ∈ ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) ↔ 𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷))))
453452eqrdv 2735 1 (𝜑 → ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) = ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1542  wex 1781  wcel 2114  wne 2933  wral 3052  wrex 3062  cin 3889  wss 3890  c0 4274  𝒫 cpw 4542  cop 4574   cuni 4851   class class class wbr 5086   Or wor 5531   × cxp 5622  dom cdm 5624  ran crn 5625  Rel wrel 5629  Fun wfun 6486   Fn wfn 6487  wf 6488  cfv 6492  (class class class)co 7360  1st c1st 7933  2nd c2nd 7934  cen 8883  Fincfn 8886  infcinf 9347  cr 11028  0cc0 11029   + caddc 11032  *cxr 11169   < clt 11170  cle 11171   / cdiv 11798  2c2 12227  +crp 12933   +𝑒 cxad 13052  PsMetcpsmet 21328  ∞Metcxmet 21329  ballcbl 21331  MetOpencmopn 21334  metUnifcmetu 21335   Cn ccn 23199  Compccmp 23361   Cnucucn 24249
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-1o 8398  df-er 8636  df-map 8768  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-sup 9348  df-inf 9349  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-n0 12429  df-z 12516  df-uz 12780  df-q 12890  df-rp 12934  df-xneg 13054  df-xadd 13055  df-xmul 13056  df-ico 13295  df-topgen 17397  df-psmet 21336  df-xmet 21337  df-bl 21339  df-mopn 21340  df-fbas 21341  df-fg 21342  df-metu 21343  df-top 22869  df-topon 22886  df-bases 22921  df-cn 23202  df-cnp 23203  df-cmp 23362  df-fil 23821  df-ust 24176  df-ucn 24250
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator