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 35739
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 5074 . . . . . . . . . . 11 (𝑑 = 𝑦 → (((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑 ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
21imbi2d 340 . . . . . . . . . 10 (𝑑 = 𝑦 → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
322ralbidv 3122 . . . . . . . . 9 (𝑑 = 𝑦 → (∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
43rexbidv 3225 . . . . . . . 8 (𝑑 = 𝑦 → (∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
54cbvralvw 3372 . . . . . . 7 (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
6 r19.12 3252 . . . . . . . 8 (∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
76ralimi 3086 . . . . . . 7 (∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
85, 7sylbi 216 . . . . . 6 (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) → ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
9 rphalfcl 12686 . . . . . . . . 9 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ+)
10 breq2 5074 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑑 / 2) → (((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦 ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
1110imbi2d 340 . . . . . . . . . . . . . . 15 (𝑦 = (𝑑 / 2) → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1211ralbidv 3120 . . . . . . . . . . . . . 14 (𝑦 = (𝑑 / 2) → (∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1312rexbidv 3225 . . . . . . . . . . . . 13 (𝑦 = (𝑑 / 2) → (∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1413ralbidv 3120 . . . . . . . . . . . 12 (𝑦 = (𝑑 / 2) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1514rspcva 3550 . . . . . . . . . . 11 (((𝑑 / 2) ∈ ℝ+ ∧ ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)) → ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
16 heicant.j . . . . . . . . . . . . . . 15 (𝜑 → (MetOpen‘𝐶) ∈ Comp)
1716ad3antrrr 726 . . . . . . . . . . . . . 14 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (MetOpen‘𝐶) ∈ Comp)
18 heicant.c . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐶 ∈ (∞Met‘𝑋))
1918ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → 𝐶 ∈ (∞Met‘𝑋))
2019anim1i 614 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) → (𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋))
21 rphalfcl 12686 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → (𝑧 / 2) ∈ ℝ+)
2221rpxrd 12702 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ℝ+ → (𝑧 / 2) ∈ ℝ*)
23 eqid 2738 . . . . . . . . . . . . . . . . . . . . . . 23 (MetOpen‘𝐶) = (MetOpen‘𝐶)
2423blopn 23562 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋 ∧ (𝑧 / 2) ∈ ℝ*) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
25243expa 1116 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧 / 2) ∈ ℝ*) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2620, 22, 25syl2an 595 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2726adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2821rpgt0d 12704 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → 0 < (𝑧 / 2))
2922, 28jca 511 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ℝ+ → ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2)))
30 xblcntr 23472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋 ∧ ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
31303expa 1116 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
3220, 29, 31syl2an 595 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
3332adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
34 opelxpi 5617 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑋 ∧ (𝑧 / 2) ∈ ℝ+) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
3521, 34sylan2 592 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑋𝑧 ∈ ℝ+) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
3635ad4ant23 749 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
37 rpcn 12669 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ ℝ+𝑧 ∈ ℂ)
38372halvesd 12149 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℝ+ → ((𝑧 / 2) + (𝑧 / 2)) = 𝑧)
3938breq2d 5082 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ℝ+ → ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) ↔ (𝑥𝐶𝑐) < 𝑧))
4039imbi1d 341 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ℝ+ → (((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
4140ralbidv 3120 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ ℝ+ → (∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
42 oveq2 7263 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑤 → (𝑥𝐶𝑐) = (𝑥𝐶𝑤))
4342breq1d 5080 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑤 → ((𝑥𝐶𝑐) < 𝑧 ↔ (𝑥𝐶𝑤) < 𝑧))
44 fveq2 6756 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 = 𝑤 → (𝑓𝑐) = (𝑓𝑤))
4544oveq2d 7271 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑤 → ((𝑓𝑥)𝐷(𝑓𝑐)) = ((𝑓𝑥)𝐷(𝑓𝑤)))
4645breq1d 5080 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑤 → (((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
4743, 46imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑤 → (((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
4847cbvralvw 3372 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐𝑋 ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
4941, 48bitrdi 286 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → (∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
5049biimpar 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 ∈ ℝ+ ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
5150adantll 710 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
52 vex 3426 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥 ∈ V
53 ovex 7288 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 / 2) ∈ V
5452, 53op1std 7814 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (1st𝑝) = 𝑥)
5552, 53op2ndd 7815 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (2nd𝑝) = (𝑧 / 2))
5654, 55oveq12d 7273 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((1st𝑝)(ball‘𝐶)(2nd𝑝)) = (𝑥(ball‘𝐶)(𝑧 / 2)))
5756eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . 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 7270 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((1st𝑝)𝐶𝑐) = (𝑥𝐶𝑐))
6055, 55oveq12d 7273 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((2nd𝑝) + (2nd𝑝)) = ((𝑧 / 2) + (𝑧 / 2)))
6159, 60breq12d 5083 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) ↔ (𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2))))
6254fveq2d 6760 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (𝑓‘(1st𝑝)) = (𝑓𝑥))
6362oveq1d 7270 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) = ((𝑓𝑥)𝐷(𝑓𝑐)))
6463breq1d 5080 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
6561, 64imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
6665ralbidv 3120 . . . . . . . . . . . . . . . . . . . . . 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 3552 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+) ∧ ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))) → ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))
6936, 51, 68syl2anc 583 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))
70 eleq2 2827 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (𝑥𝑏𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2))))
71 eqeq1 2742 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ↔ (𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝))))
7271anbi1d 629 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → ((𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7372rexbidv 3225 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7470, 73anbi12d 630 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → ((𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ (𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)) ∧ ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
7574rspcev 3552 . . . . . . . . . . . . . . . . . . 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 833 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7776rexlimdva2 3215 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) → (∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
7877ralimdva 3102 . . . . . . . . . . . . . . . 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 23502 . . . . . . . . . . . . . . . . . 18 (𝐶 ∈ (∞Met‘𝑋) → 𝑋 = (MetOpen‘𝐶))
8118, 80syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 = (MetOpen‘𝐶))
8281raleqdv 3339 . . . . . . . . . . . . . . . 16 (𝜑 → (∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
8382ad3antrrr 726 . . . . . . . . . . . . . . 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 2738 . . . . . . . . . . . . . . 15 (MetOpen‘𝐶) = (MetOpen‘𝐶)
86 fveq2 6756 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (1st𝑝) = (1st ‘(𝑔𝑏)))
87 fveq2 6756 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (2nd𝑝) = (2nd ‘(𝑔𝑏)))
8886, 87oveq12d 7273 . . . . . . . . . . . . . . . . 17 (𝑝 = (𝑔𝑏) → ((1st𝑝)(ball‘𝐶)(2nd𝑝)) = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))))
8988eqeq2d 2749 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑔𝑏) → (𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ↔ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))))
9086oveq1d 7270 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((1st𝑝)𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑐))
9187, 87oveq12d 7273 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((2nd𝑝) + (2nd𝑝)) = ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
9290, 91breq12d 5083 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) ↔ ((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
9386fveq2d 6760 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = (𝑔𝑏) → (𝑓‘(1st𝑝)) = (𝑓‘(1st ‘(𝑔𝑏))))
9493oveq1d 7270 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)))
9594breq1d 5080 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))
9692, 95imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑝 = (𝑔𝑏) → ((((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
9796ralbidv 3120 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑔𝑏) → (∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
9889, 97anbi12d 630 . . . . . . . . . . . . . . 15 (𝑝 = (𝑔𝑏) → ((𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
9985, 98cmpcovf 22450 . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . 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 4126 . . . . . . . . . . . . . 14 (𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin) → 𝑠 ∈ Fin)
103 simpll 763 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → 𝜑)
104103anim1i 614 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → (𝜑𝑠 ∈ Fin))
105 frn 6591 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran 𝑔 ⊆ (𝑋 × ℝ+))
106 rnss 5837 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ⊆ (𝑋 × ℝ+) → ran ran 𝑔 ⊆ ran (𝑋 × ℝ+))
107105, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ran (𝑋 × ℝ+))
108 rnxpss 6064 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑋 × ℝ+) ⊆ ℝ+
109107, 108sstrdi 3929 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ℝ+)
110109adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ⊆ ℝ+)
111 simplr 765 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → 𝑠 ∈ Fin)
112 ffun 6587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔:𝑠⟶(𝑋 × ℝ+) → Fun 𝑔)
113 vex 3426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑔 ∈ V
114113fundmen 8775 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun 𝑔 → dom 𝑔𝑔)
115114ensymd 8746 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Fun 𝑔𝑔 ≈ dom 𝑔)
116112, 115syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔 ≈ dom 𝑔)
117 fdm 6593 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → dom 𝑔 = 𝑠)
118116, 117breqtrd 5096 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔𝑠)
119 enfii 8932 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ Fin ∧ 𝑔𝑠) → 𝑔 ∈ Fin)
120118, 119sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ Fin ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑔 ∈ Fin)
121 rnfi 9032 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 ∈ Fin → ran 𝑔 ∈ Fin)
122 rnfi 9032 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ∈ Fin → ran ran 𝑔 ∈ Fin)
123120, 121, 1223syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ Fin ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ∈ Fin)
124111, 123sylan 579 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ∈ Fin)
125117adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → dom 𝑔 = 𝑠)
126 eqtr 2761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → 𝑋 = 𝑠)
12781, 126sylan 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑋 = 𝑠)
128 heicant.x . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑋 ≠ ∅)
129128adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑋 ≠ ∅)
130127, 129eqnetrrd 3011 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑠 ≠ ∅)
131 unieq 4847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑠 = ∅ → 𝑠 = ∅)
132 uni0 4866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ = ∅
133131, 132eqtrdi 2795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 = ∅ → 𝑠 = ∅)
134133necon3i 2975 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( 𝑠 ≠ ∅ → 𝑠 ≠ ∅)
135130, 134syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑠 ≠ ∅)
136135adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑠 ≠ ∅)
137125, 136eqnetrd 3010 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → dom 𝑔 ≠ ∅)
138 dm0rn0 5823 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑔 = ∅ ↔ ran 𝑔 = ∅)
139138necon3bii 2995 . . . . . . . . . . . . . . . . . . . . . . . . 25 (dom 𝑔 ≠ ∅ ↔ ran 𝑔 ≠ ∅)
140137, 139sylib 217 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran 𝑔 ≠ ∅)
141 relxp 5598 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Rel (𝑋 × ℝ+)
142 relss 5682 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ran 𝑔 ⊆ (𝑋 × ℝ+) → (Rel (𝑋 × ℝ+) → Rel ran 𝑔))
143105, 141, 142mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → Rel ran 𝑔)
144 relrn0 5867 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Rel ran 𝑔 → (ran 𝑔 = ∅ ↔ ran ran 𝑔 = ∅))
145144necon3bid 2987 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Rel ran 𝑔 → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
146143, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔:𝑠⟶(𝑋 × ℝ+) → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
147146adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
148140, 147mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ≠ ∅)
149148adantllr 715 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ≠ ∅)
150 rpssre 12666 . . . . . . . . . . . . . . . . . . . . . . 23 + ⊆ ℝ
151110, 150sstrdi 3929 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ⊆ ℝ)
152 ltso 10986 . . . . . . . . . . . . . . . . . . . . . . 23 < Or ℝ
153 fiinfcl 9190 . . . . . . . . . . . . . . . . . . . . . . 23 (( < Or ℝ ∧ (ran ran 𝑔 ∈ Fin ∧ ran ran 𝑔 ≠ ∅ ∧ ran ran 𝑔 ⊆ ℝ)) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
154152, 153mpan 686 . . . . . . . . . . . . . . . . . . . . . 22 ((ran ran 𝑔 ∈ Fin ∧ ran ran 𝑔 ≠ ∅ ∧ ran ran 𝑔 ⊆ ℝ) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
155124, 149, 151, 154syl3anc 1369 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
156110, 155sseldd 3918 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
157104, 156sylanl1 676 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
158157adantr 480 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
15981ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → 𝑋 = (MetOpen‘𝐶))
160159anim1i 614 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠))
161160ad2antrr 722 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠))
162 simpl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑋𝑤𝑋) → 𝑥𝑋)
163126eleq2d 2824 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑥𝑋𝑥 𝑠))
164 eluni2 4840 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 𝑠 ↔ ∃𝑏𝑠 𝑥𝑏)
165163, 164bitrdi 286 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑥𝑋 ↔ ∃𝑏𝑠 𝑥𝑏))
166165biimpa 476 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑥𝑋) → ∃𝑏𝑠 𝑥𝑏)
167161, 162, 166syl2an 595 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋)) → ∃𝑏𝑠 𝑥𝑏)
168 nfv 1918 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏(((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+))
169 nfra1 3142 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))
170168, 169nfan 1903 . . . . . . . . . . . . . . . . . . . . . 22 𝑏((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
171 nfv 1918 . . . . . . . . . . . . . . . . . . . . . 22 𝑏(𝑥𝑋𝑤𝑋)
172170, 171nfan 1903 . . . . . . . . . . . . . . . . . . . . 21 𝑏(((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋))
173 nfv 1918 . . . . . . . . . . . . . . . . . . . . 21 𝑏((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)
174 rspa 3130 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ 𝑏𝑠) → (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
175 oveq2 7263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑥 → ((1st ‘(𝑔𝑏))𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑥))
176175breq1d 5080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑥 → (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ↔ ((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
177 fveq2 6756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑐 = 𝑥 → (𝑓𝑐) = (𝑓𝑥))
178177oveq2d 7271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑥 → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
179178breq1d 5080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑥 → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)))
180176, 179imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑥 → ((((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2))))
181180rspcva 3550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑥𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)))
182 oveq2 7263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑤 → ((1st ‘(𝑔𝑏))𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑤))
183182breq1d 5080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ↔ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
18444oveq2d 7271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑤 → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
185184breq1d 5080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)))
186183, 185imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑤 → ((((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
187186rspcva 3550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑤𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)))
188181, 187anim12i 612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑥𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ (𝑤𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
189188anandirs 675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥𝑋𝑤𝑋) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
190 anim12 805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥𝑋𝑤𝑋) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
193192ad4ant23 749 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑏𝑠𝑥𝑏)) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
194 simpll 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → ((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+))
195194anim1i 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)))
196195anim1i 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)))
197109, 150sstrdi 3929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ℝ)
198197adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ran ran 𝑔 ⊆ ℝ)
199 0re 10908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 ∈ ℝ
200 rpge0 12672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 ∈ ℝ+ → 0 ≤ 𝑦)
201200rgen 3073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 𝑦 ∈ ℝ+ 0 ≤ 𝑦
202 ssralv 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (ran ran 𝑔 ⊆ ℝ+ → (∀𝑦 ∈ ℝ+ 0 ≤ 𝑦 → ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦))
203109, 201, 202mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔:𝑠⟶(𝑋 × ℝ+) → ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦)
204 breq1 5073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑥 = 0 → (𝑥𝑦 ↔ 0 ≤ 𝑦))
205204ralbidv 3120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑥 = 0 → (∀𝑦 ∈ ran ran 𝑔 𝑥𝑦 ↔ ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦))
206205rspcev 3552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((0 ∈ ℝ ∧ ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
207199, 203, 206sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑔:𝑠⟶(𝑋 × ℝ+) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
208207adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
209143adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → Rel ran 𝑔)
210 ffn 6584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔 Fn 𝑠)
211 fnfvelrn 6940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔 Fn 𝑠𝑏𝑠) → (𝑔𝑏) ∈ ran 𝑔)
212210, 211sylan 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ ran 𝑔)
213 2ndrn 7855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((Rel ran 𝑔 ∧ (𝑔𝑏) ∈ ran 𝑔) → (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔)
214209, 212, 213syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔)
215 infrelb 11890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((ran ran 𝑔 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦 ∧ (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
216198, 208, 214, 215syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
217216adantll 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
218217ad2ant2r 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
21918ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝐶 ∈ (∞Met‘𝑋))
220 xmetcl 23392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋𝑤𝑋) → (𝑥𝐶𝑤) ∈ ℝ*)
2212203expb 1118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥𝑋𝑤𝑋)) → (𝑥𝐶𝑤) ∈ ℝ*)
222219, 221sylan 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑥𝐶𝑤) ∈ ℝ*)
223222adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (𝑥𝐶𝑤) ∈ ℝ*)
224 simplr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → 𝑔:𝑠⟶(𝑋 × ℝ+))
225 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑏𝑠𝑥𝑏) → 𝑏𝑠)
226214ne0d 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ran ran 𝑔 ≠ ∅)
227 infrecl 11887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((ran ran 𝑔 ⊆ ℝ ∧ ran ran 𝑔 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ)
228198, 226, 208, 227syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ)
229228rexrd 10956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ*)
230224, 225, 229syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ*)
231 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑔:𝑠⟶(𝑋 × ℝ+))
232231ffvelrnda 6943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
233 xp2nd 7837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔𝑏) ∈ (𝑋 × ℝ+) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
234232, 233syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
235234rpxrd 12702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
236235ad2ant2r 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
237 xrltletr 12820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑥𝐶𝑤) ∈ ℝ* ∧ inf(ran ran 𝑔, ℝ, < ) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → (((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) ∧ inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
238223, 230, 236, 237syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) ∧ inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
239218, 238mpan2d 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
240239adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
24118ad6antr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝐶 ∈ (∞Met‘𝑋))
242 simpllr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → 𝑔:𝑠⟶(𝑋 × ℝ+))
243 ffvelrn 6941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
244 xp1st 7836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔𝑏) ∈ (𝑋 × ℝ+) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
245243, 244syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
246242, 225, 245syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
247 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑥𝑋𝑤𝑋) → 𝑤𝑋)
248247ad3antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝑤𝑋)
249 xmetcl 23392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑤𝑋) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
250241, 246, 248, 249syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
251250adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
252243, 233syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
253224, 252sylan 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
254253ad2ant2r 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
255254rpred 12701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
256162ad3antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝑥𝑋)
257 xmetcl 23392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑥𝑋) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
258241, 246, 256, 257syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
259252rpxrd 12702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
260242, 225, 259syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
261 eleq2 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) → (𝑥𝑏𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))))
26218ad5antr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝐶 ∈ (∞Met‘𝑋))
263224, 245sylan 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
264253rpxrd 12702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
265 elbl 23449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋 ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → (𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
266262, 263, 264, 265syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
267261, 266sylan9bbr 510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → (𝑥𝑏 ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
268267biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → (𝑥𝑏 → (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
269268an32s 648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))
273224ffvelrnda 6943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
274273, 244syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
275 simplrl 773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝑥𝑋)
276262, 274, 275, 257syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
277 xmetge0 23405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑥𝑋) → 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥))
278262, 274, 275, 277syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥))
279 xrrege0 12837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) ∧ (0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥) ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
280279an4s 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥)) ∧ ((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
281280ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥)) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
282276, 278, 281syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
283282ad2ant2r 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
284255, 272, 283mp2and 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
285284adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
286 xrltle 12812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))))
287223, 236, 286syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))))
288 xmetge0 23405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋𝑤𝑋) → 0 ≤ (𝑥𝐶𝑤))
2892883expb 1118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥𝑋𝑤𝑋)) → 0 ≤ (𝑥𝐶𝑤))
290219, 289sylan 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → 0 ≤ (𝑥𝐶𝑤))
291290adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → 0 ≤ (𝑥𝐶𝑤))
292234rpred 12701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
293292ad2ant2r 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
294 xrrege0 12837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) ∧ (0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏)))) → (𝑥𝐶𝑤) ∈ ℝ)
295294ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) → ((0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ))
296223, 293, 295syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ))
297291, 296mpand 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
298287, 297syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
299298adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
300299imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ)
301285, 300readdcld 10935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) ∈ ℝ)
302301rexrd 10956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) ∈ ℝ*)
303254, 254rpaddcld 12716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ+)
304303rpxrd 12702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ*)
305304adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ*)
306 xmettri 23412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐶 ∈ (∞Met‘𝑋) ∧ ((1st ‘(𝑔𝑏)) ∈ 𝑋𝑤𝑋𝑥𝑋)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
307241, 246, 248, 256, 306syl13anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
308307adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
309 rexadd 12895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ ∧ (𝑥𝐶𝑤) ∈ ℝ) → (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)) = (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)))
310285, 300, 309syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)) = (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)))
311308, 310breqtrd 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11528 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
316251, 302, 305, 311, 315xrlelttrd 12823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
317316ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
318252rpred 12701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
319318, 252ltaddrpd 12734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
320242, 225, 319syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
321258, 260, 304, 271, 320xrlttrd 12822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (𝜑𝑓:𝑋𝑌))
325 heicant.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑𝐷 ∈ (∞Met‘𝑌))
326 ffvelrn 6941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑓:𝑋𝑌𝑥𝑋) → (𝑓𝑥) ∈ 𝑌)
327 ffvelrn 6941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑓:𝑋𝑌𝑤𝑋) → (𝑓𝑤) ∈ 𝑌)
328326, 327anim12dan 618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑋𝑌 ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌))
329 xmetcl 23392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
3303293expb 1118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐷 ∈ (∞Met‘𝑌) ∧ ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
331325, 328, 330syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑 ∧ (𝑓:𝑋𝑌 ∧ (𝑥𝑋𝑤𝑋))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
332331anassrs 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓:𝑋𝑌) ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
333324, 332sylan 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
334333ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
335325ad5antr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝐷 ∈ (∞Met‘𝑌))
336 simp-5r 782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝑓:𝑋𝑌)
337336, 274ffvelrnd 6944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌)
338 simpllr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑓:𝑋𝑌)
339338ffvelrnda 6943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑥𝑋) → (𝑓𝑥) ∈ 𝑌)
340339adantrr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑓𝑥) ∈ 𝑌)
341340adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓𝑥) ∈ 𝑌)
342 xmetcl 23392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑥) ∈ 𝑌) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ*)
343335, 337, 341, 342syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ*)
3449rpxrd 12702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ*)
345344ad4antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑑 / 2) ∈ ℝ*)
346 xrltle 12812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ*) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)))
347343, 345, 346syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)))
348 xmetge0 23405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑥) ∈ 𝑌) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
349335, 337, 341, 348syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
3509rpred 12701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ)
351350ad4antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑑 / 2) ∈ ℝ)
352 xrrege0 12837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) ∧ (0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ)
353352ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
354343, 351, 353syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
355349, 354mpand 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
356347, 355syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
357356ad2ant2r 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
358357imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ)
359338ffvelrnda 6943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑤𝑋) → (𝑓𝑤) ∈ 𝑌)
360359adantrl 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑓𝑤) ∈ 𝑌)
361360adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓𝑤) ∈ 𝑌)
362 xmetcl 23392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ*)
363335, 337, 361, 362syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ*)
364 xrltle 12812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ*) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)))
365363, 345, 364syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)))
366 xmetge0 23405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
367335, 337, 361, 366syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
368 xrrege0 12837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) ∧ (0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ)
369368ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
370363, 351, 369syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
371367, 370mpand 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
372365, 371syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
373372ad2ant2r 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
374373imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ)
375 readdcl 10885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
376358, 374, 375syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
377376anandis 674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
378377rexrd 10956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ*)
379 rpxr 12668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 ∈ ℝ+𝑑 ∈ ℝ*)
380379ad6antlr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → 𝑑 ∈ ℝ*)
381 xmettri 23412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐷 ∈ (∞Met‘𝑌) ∧ ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌 ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
382335, 341, 361, 337, 381syl13anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
383382ad2ant2r 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
384383adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
385 xmetsym 23408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓𝑥) ∈ 𝑌 ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
386335, 341, 337, 385syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
387386ad2ant2r 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
388387adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
389388oveq1d 7270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
390 rexadd 12895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
391358, 374, 390syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
392391anandis 674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
393389, 392eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
394384, 393breqtrd 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
395 lt2add 11390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))))
398356, 372, 397syl2and 607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑑 ∈ ℝ+𝑑 ∈ ℂ)
4034022halvesd 12149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 ∈ ℝ+ → ((𝑑 / 2) + (𝑑 / 2)) = 𝑑)
404403ad6antlr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑑 / 2) + (𝑑 / 2)) = 𝑑)
405401, 404breqtrd 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < 𝑑)
406334, 378, 380, 394, 405xrlelttrd 12823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
410409adantlrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 592 . . . . . . . . . . . . . . . . . . . . . . . 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 648 . . . . . . . . . . . . . . . . . . . . 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 3114 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
420 breq2 5074 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → ((𝑥𝐶𝑤) < 𝑧 ↔ (𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < )))
421420imbi1d 341 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
4224212ralbidv 3122 . . . . . . . . . . . . . . . . . . 19 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → (∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
423422rspcev 3552 . . . . . . . . . . . . . . . . . 18 ((inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+ ∧ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
424158, 419, 423syl2anc 583 . . . . . . . . . . . . . . . . 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 1937 . . . . . . . . . . . . . . 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 592 . . . . . . . . . . . . 13 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)) → (( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
429428rexlimdva 3212 . . . . . . . . . . . 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 3106 . . . . . . 7 ((𝜑𝑓:𝑋𝑌) → ∀𝑑 ∈ ℝ+ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
435 r19.21v 3100 . . . . . . 7 (∀𝑑 ∈ ℝ+ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) ↔ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
436434, 435sylib 217 . . . . . 6 ((𝜑𝑓:𝑋𝑌) → (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
4378, 436impbid2 225 . . . . 5 ((𝜑𝑓:𝑋𝑌) → (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
438 ralcom 3280 . . . . 5 (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
439437, 438bitrdi 286 . . . 4 ((𝜑𝑓:𝑋𝑌) → (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
440439pm5.32da 578 . . 3 (𝜑 → ((𝑓:𝑋𝑌 ∧ ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
441 eqid 2738 . . . 4 (metUnif‘𝐶) = (metUnif‘𝐶)
442 eqid 2738 . . . 4 (metUnif‘𝐷) = (metUnif‘𝐷)
443 heicant.y . . . 4 (𝜑𝑌 ≠ ∅)
444 xmetpsmet 23409 . . . . 5 (𝐶 ∈ (∞Met‘𝑋) → 𝐶 ∈ (PsMet‘𝑋))
44518, 444syl 17 . . . 4 (𝜑𝐶 ∈ (PsMet‘𝑋))
446 xmetpsmet 23409 . . . . 5 (𝐷 ∈ (∞Met‘𝑌) → 𝐷 ∈ (PsMet‘𝑌))
447325, 446syl 17 . . . 4 (𝜑𝐷 ∈ (PsMet‘𝑌))
448441, 442, 128, 443, 445, 447metucn 23633 . . 3 (𝜑 → (𝑓 ∈ ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
449 eqid 2738 . . . . 5 (MetOpen‘𝐷) = (MetOpen‘𝐷)
45023, 449metcn 23605 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) → (𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
45118, 325, 450syl2anc 583 . . 3 (𝜑 → (𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
452440, 448, 4513bitr4d 310 . 2 (𝜑 → (𝑓 ∈ ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) ↔ 𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷))))
453452eqrdv 2736 1 (𝜑 → ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) = ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1085   = wceq 1539  wex 1783  wcel 2108  wne 2942  wral 3063  wrex 3064  cin 3882  wss 3883  c0 4253  𝒫 cpw 4530  cop 4564   cuni 4836   class class class wbr 5070   Or wor 5493   × cxp 5578  dom cdm 5580  ran crn 5581  Rel wrel 5585  Fun wfun 6412   Fn wfn 6413  wf 6414  cfv 6418  (class class class)co 7255  1st c1st 7802  2nd c2nd 7803  cen 8688  Fincfn 8691  infcinf 9130  cr 10801  0cc0 10802   + caddc 10805  *cxr 10939   < clt 10940  cle 10941   / cdiv 11562  2c2 11958  +crp 12659   +𝑒 cxad 12775  PsMetcpsmet 20494  ∞Metcxmet 20495  ballcbl 20497  MetOpencmopn 20500  metUnifcmetu 20501   Cn ccn 22283  Compccmp 22445   Cnucucn 23335
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879  ax-pre-sup 10880
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-er 8456  df-map 8575  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-sup 9131  df-inf 9132  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-n0 12164  df-z 12250  df-uz 12512  df-q 12618  df-rp 12660  df-xneg 12777  df-xadd 12778  df-xmul 12779  df-ico 13014  df-topgen 17071  df-psmet 20502  df-xmet 20503  df-bl 20505  df-mopn 20506  df-fbas 20507  df-fg 20508  df-metu 20509  df-top 21951  df-topon 21968  df-bases 22004  df-cn 22286  df-cnp 22287  df-cmp 22446  df-fil 22905  df-ust 23260  df-ucn 23336
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator