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 36113
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 5109 . . . . . . . . . . 11 (𝑑 = 𝑦 → (((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑 ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
21imbi2d 340 . . . . . . . . . 10 (𝑑 = 𝑦 → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
322ralbidv 3212 . . . . . . . . 9 (𝑑 = 𝑦 → (∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
43rexbidv 3175 . . . . . . . 8 (𝑑 = 𝑦 → (∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
54cbvralvw 3225 . . . . . . 7 (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
6 r19.12 3297 . . . . . . . 8 (∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
76ralimi 3086 . . . . . . 7 (∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
85, 7sylbi 216 . . . . . 6 (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) → ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
9 rphalfcl 12942 . . . . . . . . 9 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ+)
10 breq2 5109 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑑 / 2) → (((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦 ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
1110imbi2d 340 . . . . . . . . . . . . . . 15 (𝑦 = (𝑑 / 2) → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1211ralbidv 3174 . . . . . . . . . . . . . 14 (𝑦 = (𝑑 / 2) → (∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1312rexbidv 3175 . . . . . . . . . . . . 13 (𝑦 = (𝑑 / 2) → (∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1413ralbidv 3174 . . . . . . . . . . . 12 (𝑦 = (𝑑 / 2) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1514rspcva 3579 . . . . . . . . . . 11 (((𝑑 / 2) ∈ ℝ+ ∧ ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)) → ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
16 heicant.j . . . . . . . . . . . . . . 15 (𝜑 → (MetOpen‘𝐶) ∈ Comp)
1716ad3antrrr 728 . . . . . . . . . . . . . 14 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (MetOpen‘𝐶) ∈ Comp)
18 heicant.c . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐶 ∈ (∞Met‘𝑋))
1918ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → 𝐶 ∈ (∞Met‘𝑋))
2019anim1i 615 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) → (𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋))
21 rphalfcl 12942 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → (𝑧 / 2) ∈ ℝ+)
2221rpxrd 12958 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ℝ+ → (𝑧 / 2) ∈ ℝ*)
23 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . 23 (MetOpen‘𝐶) = (MetOpen‘𝐶)
2423blopn 23856 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋 ∧ (𝑧 / 2) ∈ ℝ*) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
25243expa 1118 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧 / 2) ∈ ℝ*) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2620, 22, 25syl2an 596 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2726adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2821rpgt0d 12960 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → 0 < (𝑧 / 2))
2922, 28jca 512 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ℝ+ → ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2)))
30 xblcntr 23764 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋 ∧ ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
31303expa 1118 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
3220, 29, 31syl2an 596 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
3332adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
34 opelxpi 5670 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑋 ∧ (𝑧 / 2) ∈ ℝ+) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
3521, 34sylan2 593 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑋𝑧 ∈ ℝ+) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
3635ad4ant23 751 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
37 rpcn 12925 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ ℝ+𝑧 ∈ ℂ)
38372halvesd 12399 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℝ+ → ((𝑧 / 2) + (𝑧 / 2)) = 𝑧)
3938breq2d 5117 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ℝ+ → ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) ↔ (𝑥𝐶𝑐) < 𝑧))
4039imbi1d 341 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ℝ+ → (((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
4140ralbidv 3174 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ ℝ+ → (∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
42 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑤 → (𝑥𝐶𝑐) = (𝑥𝐶𝑤))
4342breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑤 → ((𝑥𝐶𝑐) < 𝑧 ↔ (𝑥𝐶𝑤) < 𝑧))
44 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 = 𝑤 → (𝑓𝑐) = (𝑓𝑤))
4544oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑤 → ((𝑓𝑥)𝐷(𝑓𝑐)) = ((𝑓𝑥)𝐷(𝑓𝑤)))
4645breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑤 → (((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
4743, 46imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑤 → (((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
4847cbvralvw 3225 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐𝑋 ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
4941, 48bitrdi 286 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → (∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
5049biimpar 478 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 ∈ ℝ+ ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
5150adantll 712 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
52 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥 ∈ V
53 ovex 7390 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 / 2) ∈ V
5452, 53op1std 7931 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (1st𝑝) = 𝑥)
5552, 53op2ndd 7932 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (2nd𝑝) = (𝑧 / 2))
5654, 55oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((1st𝑝)(ball‘𝐶)(2nd𝑝)) = (𝑥(ball‘𝐶)(𝑧 / 2)))
5756eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)))
5857biantrurd 533 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
5954oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((1st𝑝)𝐶𝑐) = (𝑥𝐶𝑐))
6055, 55oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((2nd𝑝) + (2nd𝑝)) = ((𝑧 / 2) + (𝑧 / 2)))
6159, 60breq12d 5118 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) ↔ (𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2))))
6254fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (𝑓‘(1st𝑝)) = (𝑓𝑥))
6362oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) = ((𝑓𝑥)𝐷(𝑓𝑐)))
6463breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
6561, 64imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
6665ralbidv 3174 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
6758, 66bitr3d 280 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
6867rspcev 3581 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+) ∧ ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))) → ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))
6936, 51, 68syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))
70 eleq2 2826 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (𝑥𝑏𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2))))
71 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ↔ (𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝))))
7271anbi1d 630 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → ((𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7372rexbidv 3175 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7470, 73anbi12d 631 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → ((𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ (𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)) ∧ ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
7574rspcev 3581 . . . . . . . . . . . . . . . . . . 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 835 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7776rexlimdva2 3154 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) → (∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
7877ralimdva 3164 . . . . . . . . . . . . . . . 16 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
7978imp 407 . . . . . . . . . . . . . . 15 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
8023mopnuni 23794 . . . . . . . . . . . . . . . . . 18 (𝐶 ∈ (∞Met‘𝑋) → 𝑋 = (MetOpen‘𝐶))
8118, 80syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 = (MetOpen‘𝐶))
8281raleqdv 3313 . . . . . . . . . . . . . . . 16 (𝜑 → (∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
8382ad3antrrr 728 . . . . . . . . . . . . . . 15 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
8479, 83mpbid 231 . . . . . . . . . . . . . 14 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
85 eqid 2736 . . . . . . . . . . . . . . 15 (MetOpen‘𝐶) = (MetOpen‘𝐶)
86 fveq2 6842 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (1st𝑝) = (1st ‘(𝑔𝑏)))
87 fveq2 6842 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (2nd𝑝) = (2nd ‘(𝑔𝑏)))
8886, 87oveq12d 7375 . . . . . . . . . . . . . . . . 17 (𝑝 = (𝑔𝑏) → ((1st𝑝)(ball‘𝐶)(2nd𝑝)) = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))))
8988eqeq2d 2747 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑔𝑏) → (𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ↔ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))))
9086oveq1d 7372 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((1st𝑝)𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑐))
9187, 87oveq12d 7375 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((2nd𝑝) + (2nd𝑝)) = ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
9290, 91breq12d 5118 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) ↔ ((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
9386fveq2d 6846 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = (𝑔𝑏) → (𝑓‘(1st𝑝)) = (𝑓‘(1st ‘(𝑔𝑏))))
9493oveq1d 7372 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)))
9594breq1d 5115 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))
9692, 95imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑝 = (𝑔𝑏) → ((((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
9796ralbidv 3174 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑔𝑏) → (∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
9889, 97anbi12d 631 . . . . . . . . . . . . . . 15 (𝑝 = (𝑔𝑏) → ((𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
9985, 98cmpcovf 22742 . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . 13 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
101100ex 413 . . . . . . . . . . . 12 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))))))
102 elinel2 4156 . . . . . . . . . . . . . 14 (𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin) → 𝑠 ∈ Fin)
103 simpll 765 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → 𝜑)
104103anim1i 615 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → (𝜑𝑠 ∈ Fin))
105 frn 6675 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran 𝑔 ⊆ (𝑋 × ℝ+))
106 rnss 5894 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ⊆ (𝑋 × ℝ+) → ran ran 𝑔 ⊆ ran (𝑋 × ℝ+))
107105, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ran (𝑋 × ℝ+))
108 rnxpss 6124 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑋 × ℝ+) ⊆ ℝ+
109107, 108sstrdi 3956 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ℝ+)
110109adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ⊆ ℝ+)
111 simplr 767 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → 𝑠 ∈ Fin)
112 ffun 6671 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔:𝑠⟶(𝑋 × ℝ+) → Fun 𝑔)
113 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑔 ∈ V
114113fundmen 8975 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun 𝑔 → dom 𝑔𝑔)
115114ensymd 8945 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Fun 𝑔𝑔 ≈ dom 𝑔)
116112, 115syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔 ≈ dom 𝑔)
117 fdm 6677 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → dom 𝑔 = 𝑠)
118116, 117breqtrd 5131 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔𝑠)
119 enfii 9133 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ Fin ∧ 𝑔𝑠) → 𝑔 ∈ Fin)
120118, 119sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ Fin ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑔 ∈ Fin)
121 rnfi 9279 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 ∈ Fin → ran 𝑔 ∈ Fin)
122 rnfi 9279 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ∈ Fin → ran ran 𝑔 ∈ Fin)
123120, 121, 1223syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ Fin ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ∈ Fin)
124111, 123sylan 580 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ∈ Fin)
125117adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → dom 𝑔 = 𝑠)
126 eqtr 2759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → 𝑋 = 𝑠)
12781, 126sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑋 = 𝑠)
128 heicant.x . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑋 ≠ ∅)
129128adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑋 ≠ ∅)
130127, 129eqnetrrd 3012 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑠 ≠ ∅)
131 unieq 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑠 = ∅ → 𝑠 = ∅)
132 uni0 4896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ = ∅
133131, 132eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 = ∅ → 𝑠 = ∅)
134133necon3i 2976 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( 𝑠 ≠ ∅ → 𝑠 ≠ ∅)
135130, 134syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑠 ≠ ∅)
136135adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑠 ≠ ∅)
137125, 136eqnetrd 3011 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → dom 𝑔 ≠ ∅)
138 dm0rn0 5880 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑔 = ∅ ↔ ran 𝑔 = ∅)
139138necon3bii 2996 . . . . . . . . . . . . . . . . . . . . . . . . 25 (dom 𝑔 ≠ ∅ ↔ ran 𝑔 ≠ ∅)
140137, 139sylib 217 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran 𝑔 ≠ ∅)
141 relxp 5651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Rel (𝑋 × ℝ+)
142 relss 5737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ran 𝑔 ⊆ (𝑋 × ℝ+) → (Rel (𝑋 × ℝ+) → Rel ran 𝑔))
143105, 141, 142mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → Rel ran 𝑔)
144 relrn0 5924 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Rel ran 𝑔 → (ran 𝑔 = ∅ ↔ ran ran 𝑔 = ∅))
145144necon3bid 2988 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Rel ran 𝑔 → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
146143, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔:𝑠⟶(𝑋 × ℝ+) → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
147146adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
148140, 147mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ≠ ∅)
149148adantllr 717 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ≠ ∅)
150 rpssre 12922 . . . . . . . . . . . . . . . . . . . . . . 23 + ⊆ ℝ
151110, 150sstrdi 3956 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ⊆ ℝ)
152 ltso 11235 . . . . . . . . . . . . . . . . . . . . . . 23 < Or ℝ
153 fiinfcl 9437 . . . . . . . . . . . . . . . . . . . . . . 23 (( < Or ℝ ∧ (ran ran 𝑔 ∈ Fin ∧ ran ran 𝑔 ≠ ∅ ∧ ran ran 𝑔 ⊆ ℝ)) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
154152, 153mpan 688 . . . . . . . . . . . . . . . . . . . . . 22 ((ran ran 𝑔 ∈ Fin ∧ ran ran 𝑔 ≠ ∅ ∧ ran ran 𝑔 ⊆ ℝ) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
155124, 149, 151, 154syl3anc 1371 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
156110, 155sseldd 3945 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
157104, 156sylanl1 678 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
158157adantr 481 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
15981ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → 𝑋 = (MetOpen‘𝐶))
160159anim1i 615 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠))
161160ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠))
162 simpl 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑋𝑤𝑋) → 𝑥𝑋)
163126eleq2d 2823 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑥𝑋𝑥 𝑠))
164 eluni2 4869 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 𝑠 ↔ ∃𝑏𝑠 𝑥𝑏)
165163, 164bitrdi 286 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑥𝑋 ↔ ∃𝑏𝑠 𝑥𝑏))
166165biimpa 477 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑥𝑋) → ∃𝑏𝑠 𝑥𝑏)
167161, 162, 166syl2an 596 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋)) → ∃𝑏𝑠 𝑥𝑏)
168 nfv 1917 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏(((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+))
169 nfra1 3267 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))
170168, 169nfan 1902 . . . . . . . . . . . . . . . . . . . . . 22 𝑏((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
171 nfv 1917 . . . . . . . . . . . . . . . . . . . . . 22 𝑏(𝑥𝑋𝑤𝑋)
172170, 171nfan 1902 . . . . . . . . . . . . . . . . . . . . 21 𝑏(((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋))
173 nfv 1917 . . . . . . . . . . . . . . . . . . . . 21 𝑏((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)
174 rspa 3231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ 𝑏𝑠) → (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
175 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑥 → ((1st ‘(𝑔𝑏))𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑥))
176175breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑥 → (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ↔ ((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
177 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑐 = 𝑥 → (𝑓𝑐) = (𝑓𝑥))
178177oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑥 → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
179178breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑥 → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)))
180176, 179imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑥 → ((((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2))))
181180rspcva 3579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑥𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)))
182 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑤 → ((1st ‘(𝑔𝑏))𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑤))
183182breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ↔ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
18444oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑤 → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
185184breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)))
186183, 185imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑤 → ((((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
187186rspcva 3579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑤𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)))
188181, 187anim12i 613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑥𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ (𝑤𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
189188anandirs 677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥𝑋𝑤𝑋) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
190 anim12 807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥𝑋𝑤𝑋) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
193192ad4ant23 751 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑏𝑠𝑥𝑏)) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
194 simpll 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → ((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+))
195194anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)))
196195anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)))
197109, 150sstrdi 3956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ℝ)
198197adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ran ran 𝑔 ⊆ ℝ)
199 0re 11157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 ∈ ℝ
200 rpge0 12928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 ∈ ℝ+ → 0 ≤ 𝑦)
201200rgen 3066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 𝑦 ∈ ℝ+ 0 ≤ 𝑦
202 ssralv 4010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (ran ran 𝑔 ⊆ ℝ+ → (∀𝑦 ∈ ℝ+ 0 ≤ 𝑦 → ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦))
203109, 201, 202mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔:𝑠⟶(𝑋 × ℝ+) → ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦)
204 breq1 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑥 = 0 → (𝑥𝑦 ↔ 0 ≤ 𝑦))
205204ralbidv 3174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑥 = 0 → (∀𝑦 ∈ ran ran 𝑔 𝑥𝑦 ↔ ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦))
206205rspcev 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((0 ∈ ℝ ∧ ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
207199, 203, 206sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑔:𝑠⟶(𝑋 × ℝ+) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
208207adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
209143adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → Rel ran 𝑔)
210 ffn 6668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔 Fn 𝑠)
211 fnfvelrn 7031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔 Fn 𝑠𝑏𝑠) → (𝑔𝑏) ∈ ran 𝑔)
212210, 211sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ ran 𝑔)
213 2ndrn 7973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((Rel ran 𝑔 ∧ (𝑔𝑏) ∈ ran 𝑔) → (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔)
214209, 212, 213syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔)
215 infrelb 12140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((ran ran 𝑔 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦 ∧ (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
216198, 208, 214, 215syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
217216adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
218217ad2ant2r 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
21918ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝐶 ∈ (∞Met‘𝑋))
220 xmetcl 23684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋𝑤𝑋) → (𝑥𝐶𝑤) ∈ ℝ*)
2212203expb 1120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥𝑋𝑤𝑋)) → (𝑥𝐶𝑤) ∈ ℝ*)
222219, 221sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑥𝐶𝑤) ∈ ℝ*)
223222adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (𝑥𝐶𝑤) ∈ ℝ*)
224 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → 𝑔:𝑠⟶(𝑋 × ℝ+))
225 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑏𝑠𝑥𝑏) → 𝑏𝑠)
226214ne0d 4295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ran ran 𝑔 ≠ ∅)
227 infrecl 12137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((ran ran 𝑔 ⊆ ℝ ∧ ran ran 𝑔 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ)
228198, 226, 208, 227syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ)
229228rexrd 11205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ*)
230224, 225, 229syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ*)
231 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑔:𝑠⟶(𝑋 × ℝ+))
232231ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
233 xp2nd 7954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔𝑏) ∈ (𝑋 × ℝ+) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
234232, 233syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
235234rpxrd 12958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
236235ad2ant2r 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
237 xrltletr 13076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑥𝐶𝑤) ∈ ℝ* ∧ inf(ran ran 𝑔, ℝ, < ) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → (((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) ∧ inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
238223, 230, 236, 237syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) ∧ inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
239218, 238mpan2d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
240239adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
24118ad6antr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝐶 ∈ (∞Met‘𝑋))
242 simpllr 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → 𝑔:𝑠⟶(𝑋 × ℝ+))
243 ffvelcdm 7032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
244 xp1st 7953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔𝑏) ∈ (𝑋 × ℝ+) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
245243, 244syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
246242, 225, 245syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
247 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑥𝑋𝑤𝑋) → 𝑤𝑋)
248247ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝑤𝑋)
249 xmetcl 23684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑤𝑋) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
250241, 246, 248, 249syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
251250adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
252243, 233syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
253224, 252sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
254253ad2ant2r 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
255254rpred 12957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
256162ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝑥𝑋)
257 xmetcl 23684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑥𝑋) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
258241, 246, 256, 257syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
259252rpxrd 12958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
260242, 225, 259syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
261 eleq2 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) → (𝑥𝑏𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))))
26218ad5antr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝐶 ∈ (∞Met‘𝑋))
263224, 245sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
264253rpxrd 12958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
265 elbl 23741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋 ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → (𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
266262, 263, 264, 265syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
267261, 266sylan9bbr 511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → (𝑥𝑏 ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
268267biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → (𝑥𝑏 → (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
269268an32s 650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ 𝑏𝑠) → (𝑥𝑏 → (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
270269impr 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏))))
271270simprd 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))
272258, 260, 271xrltled 13069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))
273224ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
274273, 244syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
275 simplrl 775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝑥𝑋)
276262, 274, 275, 257syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
277 xmetge0 23697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑥𝑋) → 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥))
278262, 274, 275, 277syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥))
279 xrrege0 13093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) ∧ (0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥) ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
280279an4s 658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥)) ∧ ((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
281280ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥)) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
282276, 278, 281syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
283282ad2ant2r 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
284255, 272, 283mp2and 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
285284adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
286 xrltle 13068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))))
287223, 236, 286syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))))
288 xmetge0 23697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋𝑤𝑋) → 0 ≤ (𝑥𝐶𝑤))
2892883expb 1120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥𝑋𝑤𝑋)) → 0 ≤ (𝑥𝐶𝑤))
290219, 289sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → 0 ≤ (𝑥𝐶𝑤))
291290adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → 0 ≤ (𝑥𝐶𝑤))
292234rpred 12957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
293292ad2ant2r 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
294 xrrege0 13093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) ∧ (0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏)))) → (𝑥𝐶𝑤) ∈ ℝ)
295294ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) → ((0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ))
296223, 293, 295syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ))
297291, 296mpand 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
298287, 297syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
299298adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
300299imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ)
301285, 300readdcld 11184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) ∈ ℝ)
302301rexrd 11205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) ∈ ℝ*)
303254, 254rpaddcld 12972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ+)
304303rpxrd 12958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ*)
305304adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ*)
306 xmettri 23704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐶 ∈ (∞Met‘𝑋) ∧ ((1st ‘(𝑔𝑏)) ∈ 𝑋𝑤𝑋𝑥𝑋)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
307241, 246, 248, 256, 306syl13anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
308307adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
309 rexadd 13151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ ∧ (𝑥𝐶𝑤) ∈ ℝ) → (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)) = (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)))
310285, 300, 309syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)) = (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)))
311308, 310breqtrd 5131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)))
312255adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
313271adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))
314 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)))
315285, 300, 312, 312, 313, 314lt2addd 11778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
316251, 302, 305, 311, 315xrlelttrd 13079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
317316ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
318252rpred 12957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
319318, 252ltaddrpd 12990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
320242, 225, 319syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
321258, 260, 304, 271, 320xrlttrd 13078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
322317, 321jctild 526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (𝜑𝑓:𝑋𝑌))
325 heicant.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑𝐷 ∈ (∞Met‘𝑌))
326 ffvelcdm 7032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑓:𝑋𝑌𝑥𝑋) → (𝑓𝑥) ∈ 𝑌)
327 ffvelcdm 7032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑓:𝑋𝑌𝑤𝑋) → (𝑓𝑤) ∈ 𝑌)
328326, 327anim12dan 619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑋𝑌 ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌))
329 xmetcl 23684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
3303293expb 1120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐷 ∈ (∞Met‘𝑌) ∧ ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
331325, 328, 330syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑 ∧ (𝑓:𝑋𝑌 ∧ (𝑥𝑋𝑤𝑋))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
332331anassrs 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓:𝑋𝑌) ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
333324, 332sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
334333ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
335325ad5antr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝐷 ∈ (∞Met‘𝑌))
336 simp-5r 784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝑓:𝑋𝑌)
337336, 274ffvelcdmd 7036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌)
338 simpllr 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑓:𝑋𝑌)
339338ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑥𝑋) → (𝑓𝑥) ∈ 𝑌)
340339adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑓𝑥) ∈ 𝑌)
341340adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓𝑥) ∈ 𝑌)
342 xmetcl 23684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑥) ∈ 𝑌) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ*)
343335, 337, 341, 342syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ*)
3449rpxrd 12958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ*)
345344ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑑 / 2) ∈ ℝ*)
346 xrltle 13068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ*) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)))
347343, 345, 346syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)))
348 xmetge0 23697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑥) ∈ 𝑌) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
349335, 337, 341, 348syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
3509rpred 12957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ)
351350ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑑 / 2) ∈ ℝ)
352 xrrege0 13093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) ∧ (0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ)
353352ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
354343, 351, 353syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
355349, 354mpand 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
356347, 355syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
357356ad2ant2r 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
358357imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ)
359338ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑤𝑋) → (𝑓𝑤) ∈ 𝑌)
360359adantrl 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑓𝑤) ∈ 𝑌)
361360adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓𝑤) ∈ 𝑌)
362 xmetcl 23684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ*)
363335, 337, 361, 362syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ*)
364 xrltle 13068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ*) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)))
365363, 345, 364syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)))
366 xmetge0 23697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
367335, 337, 361, 366syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
368 xrrege0 13093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) ∧ (0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ)
369368ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
370363, 351, 369syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
371367, 370mpand 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
372365, 371syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
373372ad2ant2r 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
374373imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ)
375 readdcl 11134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
376358, 374, 375syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
377376anandis 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
378377rexrd 11205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ*)
379 rpxr 12924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 ∈ ℝ+𝑑 ∈ ℝ*)
380379ad6antlr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → 𝑑 ∈ ℝ*)
381 xmettri 23704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐷 ∈ (∞Met‘𝑌) ∧ ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌 ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
382335, 341, 361, 337, 381syl13anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
383382ad2ant2r 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
384383adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
385 xmetsym 23700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓𝑥) ∈ 𝑌 ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
386335, 341, 337, 385syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
387386ad2ant2r 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
388387adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
389388oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
390 rexadd 13151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
391358, 374, 390syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
392391anandis 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
393389, 392eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
394384, 393breqtrd 5131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
395 lt2add 11640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) ∧ ((𝑑 / 2) ∈ ℝ ∧ (𝑑 / 2) ∈ ℝ)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2))))
396395expcom 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑑 / 2) ∈ ℝ ∧ (𝑑 / 2) ∈ ℝ) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))))
397351, 351, 396syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))))
398356, 372, 397syl2and 608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2))))
401400imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))
402 rpcn 12925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑑 ∈ ℝ+𝑑 ∈ ℂ)
4034022halvesd 12399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 ∈ ℝ+ → ((𝑑 / 2) + (𝑑 / 2)) = 𝑑)
404403ad6antlr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑑 / 2) + (𝑑 / 2)) = 𝑑)
405401, 404breqtrd 5131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < 𝑑)
406334, 378, 380, 394, 405xrlelttrd 13079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)
407406ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
410409adantlrr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 421 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
413174, 412sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ 𝑏𝑠)) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
414413expr 457 . . . . . . . . . . . . . . . . . . . . . . 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 650 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋)) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
417172, 173, 416rexlimd 3249 . . . . . . . . . . . . . . . . . . . 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 3197 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
420 breq2 5109 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → ((𝑥𝐶𝑤) < 𝑧 ↔ (𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < )))
421420imbi1d 341 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
4224212ralbidv 3212 . . . . . . . . . . . . . . . . . . 19 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → (∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
423422rspcev 3581 . . . . . . . . . . . . . . . . . 18 ((inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+ ∧ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
424158, 419, 423syl2anc 584 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
425424expl 458 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
426425exlimdv 1936 . . . . . . . . . . . . . . 15 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → (∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
427426expimpd 454 . . . . . . . . . . . . . 14 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → (( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
428102, 427sylan2 593 . . . . . . . . . . . . 13 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)) → (( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
429428rexlimdva 3152 . . . . . . . . . . . 12 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
430101, 429syld 47 . . . . . . . . . . 11 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
43115, 430syl5 34 . . . . . . . . . 10 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (((𝑑 / 2) ∈ ℝ+ ∧ ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
432431exp4b 431 . . . . . . . . 9 ((𝜑𝑓:𝑋𝑌) → (𝑑 ∈ ℝ+ → ((𝑑 / 2) ∈ ℝ+ → (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))))
4339, 432mpdi 45 . . . . . . . 8 ((𝜑𝑓:𝑋𝑌) → (𝑑 ∈ ℝ+ → (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
434433ralrimiv 3142 . . . . . . 7 ((𝜑𝑓:𝑋𝑌) → ∀𝑑 ∈ ℝ+ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
435 r19.21v 3176 . . . . . . 7 (∀𝑑 ∈ ℝ+ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) ↔ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
436434, 435sylib 217 . . . . . 6 ((𝜑𝑓:𝑋𝑌) → (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
4378, 436impbid2 225 . . . . 5 ((𝜑𝑓:𝑋𝑌) → (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
438 ralcom 3272 . . . . 5 (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
439437, 438bitrdi 286 . . . 4 ((𝜑𝑓:𝑋𝑌) → (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
440439pm5.32da 579 . . 3 (𝜑 → ((𝑓:𝑋𝑌 ∧ ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
441 eqid 2736 . . . 4 (metUnif‘𝐶) = (metUnif‘𝐶)
442 eqid 2736 . . . 4 (metUnif‘𝐷) = (metUnif‘𝐷)
443 heicant.y . . . 4 (𝜑𝑌 ≠ ∅)
444 xmetpsmet 23701 . . . . 5 (𝐶 ∈ (∞Met‘𝑋) → 𝐶 ∈ (PsMet‘𝑋))
44518, 444syl 17 . . . 4 (𝜑𝐶 ∈ (PsMet‘𝑋))
446 xmetpsmet 23701 . . . . 5 (𝐷 ∈ (∞Met‘𝑌) → 𝐷 ∈ (PsMet‘𝑌))
447325, 446syl 17 . . . 4 (𝜑𝐷 ∈ (PsMet‘𝑌))
448441, 442, 128, 443, 445, 447metucn 23927 . . 3 (𝜑 → (𝑓 ∈ ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
449 eqid 2736 . . . . 5 (MetOpen‘𝐷) = (MetOpen‘𝐷)
45023, 449metcn 23899 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) → (𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
45118, 325, 450syl2anc 584 . . 3 (𝜑 → (𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
452440, 448, 4513bitr4d 310 . 2 (𝜑 → (𝑓 ∈ ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) ↔ 𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷))))
453452eqrdv 2734 1 (𝜑 → ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) = ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2943  wral 3064  wrex 3073  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560  cop 4592   cuni 4865   class class class wbr 5105   Or wor 5544   × cxp 5631  dom cdm 5633  ran crn 5634  Rel wrel 5638  Fun wfun 6490   Fn wfn 6491  wf 6492  cfv 6496  (class class class)co 7357  1st c1st 7919  2nd c2nd 7920  cen 8880  Fincfn 8883  infcinf 9377  cr 11050  0cc0 11051   + caddc 11054  *cxr 11188   < clt 11189  cle 11190   / cdiv 11812  2c2 12208  +crp 12915   +𝑒 cxad 13031  PsMetcpsmet 20780  ∞Metcxmet 20781  ballcbl 20783  MetOpencmopn 20786  metUnifcmetu 20787   Cn ccn 22575  Compccmp 22737   Cnucucn 23627
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-n0 12414  df-z 12500  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ico 13270  df-topgen 17325  df-psmet 20788  df-xmet 20789  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-metu 20795  df-top 22243  df-topon 22260  df-bases 22296  df-cn 22578  df-cnp 22579  df-cmp 22738  df-fil 23197  df-ust 23552  df-ucn 23628
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator