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 32614
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 4587 . . . . . . . . . . 11 (𝑑 = 𝑦 → (((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑 ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
21imbi2d 329 . . . . . . . . . 10 (𝑑 = 𝑦 → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
322ralbidv 2972 . . . . . . . . 9 (𝑑 = 𝑦 → (∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
43rexbidv 3034 . . . . . . . 8 (𝑑 = 𝑦 → (∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
54cbvralv 3147 . . . . . . 7 (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
6 r19.12 3045 . . . . . . . 8 (∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
76ralimi 2936 . . . . . . 7 (∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
85, 7sylbi 206 . . . . . 6 (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) → ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
9 rphalfcl 11734 . . . . . . . . 9 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ+)
10 breq2 4587 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑑 / 2) → (((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦 ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
1110imbi2d 329 . . . . . . . . . . . . . . 15 (𝑦 = (𝑑 / 2) → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1211ralbidv 2969 . . . . . . . . . . . . . 14 (𝑦 = (𝑑 / 2) → (∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1312rexbidv 3034 . . . . . . . . . . . . 13 (𝑦 = (𝑑 / 2) → (∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1413ralbidv 2969 . . . . . . . . . . . 12 (𝑦 = (𝑑 / 2) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1514rspcva 3280 . . . . . . . . . . 11 (((𝑑 / 2) ∈ ℝ+ ∧ ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)) → ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
16 heicant.j . . . . . . . . . . . . . . 15 (𝜑 → (MetOpen‘𝐶) ∈ Comp)
1716ad3antrrr 762 . . . . . . . . . . . . . 14 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (MetOpen‘𝐶) ∈ Comp)
18 heicant.c . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐶 ∈ (∞Met‘𝑋))
1918ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → 𝐶 ∈ (∞Met‘𝑋))
2019anim1i 590 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) → (𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋))
21 rphalfcl 11734 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ ℝ+ → (𝑧 / 2) ∈ ℝ+)
2221rpxrd 11749 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → (𝑧 / 2) ∈ ℝ*)
23 eqid 2610 . . . . . . . . . . . . . . . . . . . . . . . 24 (MetOpen‘𝐶) = (MetOpen‘𝐶)
2423blopn 22115 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋 ∧ (𝑧 / 2) ∈ ℝ*) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
25243expa 1257 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧 / 2) ∈ ℝ*) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2620, 22, 25syl2an 493 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2726adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2821rpgt0d 11751 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ ℝ+ → 0 < (𝑧 / 2))
2922, 28jca 553 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2)))
30 xblcntr 22026 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋 ∧ ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
31303expa 1257 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
3220, 29, 31syl2an 493 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
3332adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
34 opelxpi 5072 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝑋 ∧ (𝑧 / 2) ∈ ℝ+) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
3521, 34sylan2 490 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑋𝑧 ∈ ℝ+) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
3635ad4ant23 1289 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
37 rpcn 11717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ ℝ+𝑧 ∈ ℂ)
38372halvesd 11155 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ ℝ+ → ((𝑧 / 2) + (𝑧 / 2)) = 𝑧)
3938breq2d 4595 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℝ+ → ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) ↔ (𝑥𝐶𝑐) < 𝑧))
4039imbi1d 330 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ℝ+ → (((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
4140ralbidv 2969 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ℝ+ → (∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
42 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 = 𝑤 → (𝑥𝐶𝑐) = (𝑥𝐶𝑤))
4342breq1d 4593 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑤 → ((𝑥𝐶𝑐) < 𝑧 ↔ (𝑥𝐶𝑤) < 𝑧))
44 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = 𝑤 → (𝑓𝑐) = (𝑓𝑤))
4544oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 = 𝑤 → ((𝑓𝑥)𝐷(𝑓𝑐)) = ((𝑓𝑥)𝐷(𝑓𝑤)))
4645breq1d 4593 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑤 → (((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
4743, 46imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑤 → (((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
4847cbvralv 3147 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑐𝑋 ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
4941, 48syl6bb 275 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ ℝ+ → (∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
5049biimpar 501 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 ∈ ℝ+ ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
5150adantll 746 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
52 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ∈ V
53 ovex 6577 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 / 2) ∈ V
5452, 53op1std 7069 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (1st𝑝) = 𝑥)
5552, 53op2ndd 7070 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (2nd𝑝) = (𝑧 / 2))
5654, 55oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((1st𝑝)(ball‘𝐶)(2nd𝑝)) = (𝑥(ball‘𝐶)(𝑧 / 2)))
5756eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)))
5857biantrurd 528 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
5954oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((1st𝑝)𝐶𝑐) = (𝑥𝐶𝑐))
6055, 55oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((2nd𝑝) + (2nd𝑝)) = ((𝑧 / 2) + (𝑧 / 2)))
6159, 60breq12d 4596 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) ↔ (𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2))))
6254fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (𝑓‘(1st𝑝)) = (𝑓𝑥))
6362oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) = ((𝑓𝑥)𝐷(𝑓𝑐)))
6463breq1d 4593 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
6561, 64imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
6665ralbidv 2969 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
6758, 66bitr3d 269 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
6867rspcev 3282 . . . . . . . . . . . . . . . . . . . . 21 ((⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+) ∧ ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))) → ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))
6936, 51, 68syl2anc 691 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))
70 eleq2 2677 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (𝑥𝑏𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2))))
71 eqeq1 2614 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ↔ (𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝))))
7271anbi1d 737 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → ((𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7372rexbidv 3034 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7470, 73anbi12d 743 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → ((𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ (𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)) ∧ ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
7574rspcev 3282 . . . . . . . . . . . . . . . . . . . 20 (((𝑥(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 1316 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7776ex 449 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) → (∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
7877rexlimdva 3013 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) → (∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
7978ralimdva 2945 . . . . . . . . . . . . . . . 16 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
8079imp 444 . . . . . . . . . . . . . . 15 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
8123mopnuni 22056 . . . . . . . . . . . . . . . . . 18 (𝐶 ∈ (∞Met‘𝑋) → 𝑋 = (MetOpen‘𝐶))
8218, 81syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 = (MetOpen‘𝐶))
8382raleqdv 3121 . . . . . . . . . . . . . . . 16 (𝜑 → (∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
8483ad3antrrr 762 . . . . . . . . . . . . . . 15 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
8580, 84mpbid 221 . . . . . . . . . . . . . 14 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
86 eqid 2610 . . . . . . . . . . . . . . 15 (MetOpen‘𝐶) = (MetOpen‘𝐶)
87 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (1st𝑝) = (1st ‘(𝑔𝑏)))
88 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (2nd𝑝) = (2nd ‘(𝑔𝑏)))
8987, 88oveq12d 6567 . . . . . . . . . . . . . . . . 17 (𝑝 = (𝑔𝑏) → ((1st𝑝)(ball‘𝐶)(2nd𝑝)) = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))))
9089eqeq2d 2620 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑔𝑏) → (𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ↔ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))))
9187oveq1d 6564 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((1st𝑝)𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑐))
9288, 88oveq12d 6567 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((2nd𝑝) + (2nd𝑝)) = ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
9391, 92breq12d 4596 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) ↔ ((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
9487fveq2d 6107 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = (𝑔𝑏) → (𝑓‘(1st𝑝)) = (𝑓‘(1st ‘(𝑔𝑏))))
9594oveq1d 6564 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)))
9695breq1d 4593 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))
9793, 96imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑝 = (𝑔𝑏) → ((((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
9897ralbidv 2969 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑔𝑏) → (∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
9990, 98anbi12d 743 . . . . . . . . . . . . . . 15 (𝑝 = (𝑔𝑏) → ((𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
10086, 99cmpcovf 21004 . . . . . . . . . . . . . 14 (((MetOpen‘𝐶) ∈ Comp ∧ ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
10117, 85, 100syl2anc 691 . . . . . . . . . . . . 13 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
102101ex 449 . . . . . . . . . . . 12 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))))))
103 elinel2 3762 . . . . . . . . . . . . . 14 (𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin) → 𝑠 ∈ Fin)
104 simpll 786 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → 𝜑)
105104anim1i 590 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → (𝜑𝑠 ∈ Fin))
106 frn 5966 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran 𝑔 ⊆ (𝑋 × ℝ+))
107 rnss 5275 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ⊆ (𝑋 × ℝ+) → ran ran 𝑔 ⊆ ran (𝑋 × ℝ+))
108106, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ran (𝑋 × ℝ+))
109 rnxpss 5485 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑋 × ℝ+) ⊆ ℝ+
110108, 109syl6ss 3580 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ℝ+)
111110adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ⊆ ℝ+)
112 simplr 788 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → 𝑠 ∈ Fin)
113 ffun 5961 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔:𝑠⟶(𝑋 × ℝ+) → Fun 𝑔)
114 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑔 ∈ V
115114fundmen 7916 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun 𝑔 → dom 𝑔𝑔)
116115ensymd 7893 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Fun 𝑔𝑔 ≈ dom 𝑔)
117113, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔 ≈ dom 𝑔)
118 fdm 5964 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → dom 𝑔 = 𝑠)
119117, 118breqtrd 4609 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔𝑠)
120 enfii 8062 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ Fin ∧ 𝑔𝑠) → 𝑔 ∈ Fin)
121119, 120sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ Fin ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑔 ∈ Fin)
122 rnfi 8132 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 ∈ Fin → ran 𝑔 ∈ Fin)
123 rnfi 8132 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ∈ Fin → ran ran 𝑔 ∈ Fin)
124121, 122, 1233syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ Fin ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ∈ Fin)
125112, 124sylan 487 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ∈ Fin)
126118adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → dom 𝑔 = 𝑠)
127 eqtr 2629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → 𝑋 = 𝑠)
12882, 127sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑋 = 𝑠)
129 heicant.x . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑋 ≠ ∅)
130129adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑋 ≠ ∅)
131128, 130eqnetrrd 2850 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑠 ≠ ∅)
132 unieq 4380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑠 = ∅ → 𝑠 = ∅)
133 uni0 4401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ = ∅
134132, 133syl6eq 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 = ∅ → 𝑠 = ∅)
135134necon3i 2814 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( 𝑠 ≠ ∅ → 𝑠 ≠ ∅)
136131, 135syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑠 ≠ ∅)
137136adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑠 ≠ ∅)
138126, 137eqnetrd 2849 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → dom 𝑔 ≠ ∅)
139 dm0rn0 5263 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑔 = ∅ ↔ ran 𝑔 = ∅)
140139necon3bii 2834 . . . . . . . . . . . . . . . . . . . . . . . . 25 (dom 𝑔 ≠ ∅ ↔ ran 𝑔 ≠ ∅)
141138, 140sylib 207 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran 𝑔 ≠ ∅)
142 relxp 5150 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Rel (𝑋 × ℝ+)
143 relss 5129 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ran 𝑔 ⊆ (𝑋 × ℝ+) → (Rel (𝑋 × ℝ+) → Rel ran 𝑔))
144106, 142, 143mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → Rel ran 𝑔)
145 relrn0 5304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Rel ran 𝑔 → (ran 𝑔 = ∅ ↔ ran ran 𝑔 = ∅))
146145necon3bid 2826 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Rel ran 𝑔 → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
147144, 146syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔:𝑠⟶(𝑋 × ℝ+) → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
148147adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
149141, 148mpbid 221 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ≠ ∅)
150149adantllr 751 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ≠ ∅)
151 rpssre 11719 . . . . . . . . . . . . . . . . . . . . . . 23 + ⊆ ℝ
152111, 151syl6ss 3580 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ⊆ ℝ)
153 ltso 9997 . . . . . . . . . . . . . . . . . . . . . . 23 < Or ℝ
154 fiinfcl 8290 . . . . . . . . . . . . . . . . . . . . . . 23 (( < Or ℝ ∧ (ran ran 𝑔 ∈ Fin ∧ ran ran 𝑔 ≠ ∅ ∧ ran ran 𝑔 ⊆ ℝ)) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
155153, 154mpan 702 . . . . . . . . . . . . . . . . . . . . . 22 ((ran ran 𝑔 ∈ Fin ∧ ran ran 𝑔 ≠ ∅ ∧ ran ran 𝑔 ⊆ ℝ) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
156125, 150, 152, 155syl3anc 1318 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
157111, 156sseldd 3569 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
158105, 157sylanl1 680 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
159158adantr 480 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
16082ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → 𝑋 = (MetOpen‘𝐶))
161160anim1i 590 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠))
162161ad2antrr 758 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠))
163 simpl 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑋𝑤𝑋) → 𝑥𝑋)
164127eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑥𝑋𝑥 𝑠))
165 eluni2 4376 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 𝑠 ↔ ∃𝑏𝑠 𝑥𝑏)
166164, 165syl6bb 275 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑥𝑋 ↔ ∃𝑏𝑠 𝑥𝑏))
167166biimpa 500 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑥𝑋) → ∃𝑏𝑠 𝑥𝑏)
168162, 163, 167syl2an 493 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋)) → ∃𝑏𝑠 𝑥𝑏)
169 nfv 1830 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏(((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+))
170 nfra1 2925 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))
171169, 170nfan 1816 . . . . . . . . . . . . . . . . . . . . . 22 𝑏((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
172 nfv 1830 . . . . . . . . . . . . . . . . . . . . . 22 𝑏(𝑥𝑋𝑤𝑋)
173171, 172nfan 1816 . . . . . . . . . . . . . . . . . . . . 21 𝑏(((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋))
174 nfv 1830 . . . . . . . . . . . . . . . . . . . . 21 𝑏((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)
175 rspa 2914 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ 𝑏𝑠) → (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
176 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑥 → ((1st ‘(𝑔𝑏))𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑥))
177176breq1d 4593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑥 → (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ↔ ((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
178 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑐 = 𝑥 → (𝑓𝑐) = (𝑓𝑥))
179178oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑥 → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
180179breq1d 4593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑥 → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)))
181177, 180imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑥 → ((((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2))))
182181rspcva 3280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑥𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)))
183 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑤 → ((1st ‘(𝑔𝑏))𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑤))
184183breq1d 4593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ↔ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
18544oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑤 → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
186185breq1d 4593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)))
187184, 186imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑤 → ((((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
188187rspcva 3280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑤𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)))
189182, 188anim12i 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑥𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ (𝑤𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
190189anandirs 870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥𝑋𝑤𝑋) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
191 prth 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
192190, 191syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥𝑋𝑤𝑋) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
193192adantrl 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥𝑋𝑤𝑋) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
194193ad4ant23 1289 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑏𝑠𝑥𝑏)) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
195 simpll 786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → ((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+))
196195anim1i 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)))
197196anim1i 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)))
198110, 151syl6ss 3580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ℝ)
199198adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ran ran 𝑔 ⊆ ℝ)
200 0re 9919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 ∈ ℝ
201 rpge0 11721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 ∈ ℝ+ → 0 ≤ 𝑦)
202201rgen 2906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 𝑦 ∈ ℝ+ 0 ≤ 𝑦
203 ssralv 3629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (ran ran 𝑔 ⊆ ℝ+ → (∀𝑦 ∈ ℝ+ 0 ≤ 𝑦 → ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦))
204110, 202, 203mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔:𝑠⟶(𝑋 × ℝ+) → ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦)
205 breq1 4586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑥 = 0 → (𝑥𝑦 ↔ 0 ≤ 𝑦))
206205ralbidv 2969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑥 = 0 → (∀𝑦 ∈ ran ran 𝑔 𝑥𝑦 ↔ ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦))
207206rspcev 3282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((0 ∈ ℝ ∧ ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
208200, 204, 207sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑔:𝑠⟶(𝑋 × ℝ+) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
209208adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
210144adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → Rel ran 𝑔)
211 ffn 5958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔 Fn 𝑠)
212 fnfvelrn 6264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔 Fn 𝑠𝑏𝑠) → (𝑔𝑏) ∈ ran 𝑔)
213211, 212sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ ran 𝑔)
214 2ndrn 7107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((Rel ran 𝑔 ∧ (𝑔𝑏) ∈ ran 𝑔) → (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔)
215210, 213, 214syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔)
216 infrelb 10885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((ran ran 𝑔 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦 ∧ (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
217199, 209, 215, 216syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
218217adantll 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
219218ad2ant2r 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
22018ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝐶 ∈ (∞Met‘𝑋))
221 xmetcl 21946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋𝑤𝑋) → (𝑥𝐶𝑤) ∈ ℝ*)
2222213expb 1258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥𝑋𝑤𝑋)) → (𝑥𝐶𝑤) ∈ ℝ*)
223220, 222sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑥𝐶𝑤) ∈ ℝ*)
224223adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (𝑥𝐶𝑤) ∈ ℝ*)
225 simplr 788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → 𝑔:𝑠⟶(𝑋 × ℝ+))
226 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑏𝑠𝑥𝑏) → 𝑏𝑠)
227 ne0i 3880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔 → ran ran 𝑔 ≠ ∅)
228215, 227syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ran ran 𝑔 ≠ ∅)
229 infrecl 10882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((ran ran 𝑔 ⊆ ℝ ∧ ran ran 𝑔 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ)
230199, 228, 209, 229syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ)
231230rexrd 9968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ*)
232225, 226, 231syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ*)
233 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑔:𝑠⟶(𝑋 × ℝ+))
234233ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
235 xp2nd 7090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔𝑏) ∈ (𝑋 × ℝ+) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
236234, 235syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
237236rpxrd 11749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
238237ad2ant2r 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
239 xrltletr 11864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑥𝐶𝑤) ∈ ℝ* ∧ inf(ran ran 𝑔, ℝ, < ) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → (((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) ∧ inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
240224, 232, 238, 239syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) ∧ inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
241219, 240mpan2d 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
242241adantlr 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
24318ad6antr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝐶 ∈ (∞Met‘𝑋))
244 simpllr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → 𝑔:𝑠⟶(𝑋 × ℝ+))
245 ffvelrn 6265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
246 xp1st 7089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔𝑏) ∈ (𝑋 × ℝ+) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
247245, 246syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
248244, 226, 247syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
249 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑥𝑋𝑤𝑋) → 𝑤𝑋)
250249ad3antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝑤𝑋)
251 xmetcl 21946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑤𝑋) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
252243, 248, 250, 251syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
253252adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
254245, 235syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
255225, 254sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
256255ad2ant2r 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
257256rpred 11748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
258 eleq2 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) → (𝑥𝑏𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))))
25918ad5antr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝐶 ∈ (∞Met‘𝑋))
260225, 247sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
261255rpxrd 11749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
262 elbl 22003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋 ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → (𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
263259, 260, 261, 262syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
264258, 263sylan9bbr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → (𝑥𝑏 ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
265264biimpd 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → (𝑥𝑏 → (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
266265an32s 842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ 𝑏𝑠) → (𝑥𝑏 → (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
267266impr 647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏))))
268267simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))
269163ad3antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝑥𝑋)
270 xmetcl 21946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑥𝑋) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
271243, 248, 269, 270syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
272254rpxrd 11749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
273244, 226, 272syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
274 xrltle 11858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → (((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))))
275271, 273, 274syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))))
276268, 275mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))
277225ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
278277, 246syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
279 simplrl 796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝑥𝑋)
280259, 278, 279, 270syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
281 xmetge0 21959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑥𝑋) → 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥))
282259, 278, 279, 281syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥))
283 xrrege0 11879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) ∧ (0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥) ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
284283an4s 865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥)) ∧ ((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
285284ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥)) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
286280, 282, 285syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
287286ad2ant2r 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
288257, 276, 287mp2and 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
289288adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
290 xrltle 11858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))))
291224, 238, 290syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))))
292 xmetge0 21959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋𝑤𝑋) → 0 ≤ (𝑥𝐶𝑤))
2932923expb 1258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥𝑋𝑤𝑋)) → 0 ≤ (𝑥𝐶𝑤))
294220, 293sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → 0 ≤ (𝑥𝐶𝑤))
295294adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → 0 ≤ (𝑥𝐶𝑤))
296236rpred 11748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
297296ad2ant2r 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
298 xrrege0 11879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) ∧ (0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏)))) → (𝑥𝐶𝑤) ∈ ℝ)
299298ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) → ((0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ))
300224, 297, 299syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ))
301295, 300mpand 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
302291, 301syld 46 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
303302adantlr 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
304303imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ)
305289, 304readdcld 9948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) ∈ ℝ)
306305rexrd 9968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) ∈ ℝ*)
307256, 256rpaddcld 11763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ+)
308307rpxrd 11749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ*)
309308adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ*)
310 xmettri 21966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐶 ∈ (∞Met‘𝑋) ∧ ((1st ‘(𝑔𝑏)) ∈ 𝑋𝑤𝑋𝑥𝑋)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
311243, 248, 250, 269, 310syl13anc 1320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
312311adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
313 rexadd 11937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ ∧ (𝑥𝐶𝑤) ∈ ℝ) → (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)) = (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)))
314289, 304, 313syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)) = (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)))
315312, 314breqtrd 4609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)))
316257adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
317268adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))
318 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)))
319289, 304, 316, 316, 317, 318lt2addd 10529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
320253, 306, 309, 315, 319xrlelttrd 11867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
321320ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
322254rpred 11748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
323322, 254ltaddrpd 11781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
324244, 226, 323syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
325271, 273, 308, 268, 324xrlttrd 11866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
326321, 325jctild 564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))))
327242, 326syld 46 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))))
328 simpll 786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (𝜑𝑓:𝑋𝑌))
329 heicant.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑𝐷 ∈ (∞Met‘𝑌))
330 ffvelrn 6265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑓:𝑋𝑌𝑥𝑋) → (𝑓𝑥) ∈ 𝑌)
331 ffvelrn 6265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑓:𝑋𝑌𝑤𝑋) → (𝑓𝑤) ∈ 𝑌)
332330, 331anim12dan 878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑋𝑌 ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌))
333 xmetcl 21946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
3343333expb 1258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐷 ∈ (∞Met‘𝑌) ∧ ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
335329, 332, 334syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑 ∧ (𝑓:𝑋𝑌 ∧ (𝑥𝑋𝑤𝑋))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
336335anassrs 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓:𝑋𝑌) ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
337328, 336sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
338337ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
339329ad5antr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝐷 ∈ (∞Met‘𝑌))
340 simp-5r 805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝑓:𝑋𝑌)
341340, 278ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌)
342 simpllr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑓:𝑋𝑌)
343342ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑥𝑋) → (𝑓𝑥) ∈ 𝑌)
344343adantrr 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑓𝑥) ∈ 𝑌)
345344adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓𝑥) ∈ 𝑌)
346 xmetcl 21946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑥) ∈ 𝑌) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ*)
347339, 341, 345, 346syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ*)
3489rpxrd 11749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ*)
349348ad4antlr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑑 / 2) ∈ ℝ*)
350 xrltle 11858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ*) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)))
351347, 349, 350syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)))
352 xmetge0 21959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑥) ∈ 𝑌) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
353339, 341, 345, 352syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
3549rpred 11748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ)
355354ad4antlr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑑 / 2) ∈ ℝ)
356 xrrege0 11879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) ∧ (0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ)
357356ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
358347, 355, 357syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
359353, 358mpand 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
360351, 359syld 46 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
361360ad2ant2r 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
362361imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ)
363342ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑤𝑋) → (𝑓𝑤) ∈ 𝑌)
364363adantrl 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑓𝑤) ∈ 𝑌)
365364adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓𝑤) ∈ 𝑌)
366 xmetcl 21946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ*)
367339, 341, 365, 366syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ*)
368 xrltle 11858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ*) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)))
369367, 349, 368syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)))
370 xmetge0 21959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
371339, 341, 365, 370syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
372 xrrege0 11879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) ∧ (0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ)
373372ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
374367, 355, 373syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
375371, 374mpand 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
376369, 375syld 46 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
377376ad2ant2r 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
378377imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ)
379 readdcl 9898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
380362, 378, 379syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
381380anandis 869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
382381rexrd 9968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ*)
383 rpxr 11716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 ∈ ℝ+𝑑 ∈ ℝ*)
384383ad6antlr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → 𝑑 ∈ ℝ*)
385 xmettri 21966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐷 ∈ (∞Met‘𝑌) ∧ ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌 ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
386339, 345, 365, 341, 385syl13anc 1320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
387386ad2ant2r 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
388387adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
389 xmetsym 21962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓𝑥) ∈ 𝑌 ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
390339, 345, 341, 389syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
391390ad2ant2r 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
392391adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
393392oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
394 rexadd 11937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
395362, 378, 394syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
396395anandis 869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
397393, 396eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
398388, 397breqtrd 4609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
399 lt2add 10392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) ∧ ((𝑑 / 2) ∈ ℝ ∧ (𝑑 / 2) ∈ ℝ)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2))))
400399expcom 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑑 / 2) ∈ ℝ ∧ (𝑑 / 2) ∈ ℝ) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))))
401355, 355, 400syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))))
402360, 376, 401syl2and 499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))))
403402pm2.43d 51 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2))))
404403ad2ant2r 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2))))
405404imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))
406 rpcn 11717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑑 ∈ ℝ+𝑑 ∈ ℂ)
4074062halvesd 11155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 ∈ ℝ+ → ((𝑑 / 2) + (𝑑 / 2)) = 𝑑)
408407ad6antlr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑑 / 2) + (𝑑 / 2)) = 𝑑)
409405, 408breqtrd 4609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < 𝑑)
410338, 382, 384, 398, 409xrlelttrd 11867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)
411410ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
412327, 411imim12d 79 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
413197, 412sylanl1 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
414413adantlrr 753 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑏𝑠𝑥𝑏)) → (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
415194, 414mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
416415exp32 629 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
417175, 416sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ 𝑏𝑠)) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
418417expr 641 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑏𝑠 → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))))
419418pm2.43d 51 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
420419an32s 842 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋)) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
421173, 174, 420rexlimd 3008 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋)) → (∃𝑏𝑠 𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
422168, 421mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
423422ralrimivva 2954 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
424 breq2 4587 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → ((𝑥𝐶𝑤) < 𝑧 ↔ (𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < )))
425424imbi1d 330 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
4264252ralbidv 2972 . . . . . . . . . . . . . . . . . . 19 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → (∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
427426rspcev 3282 . . . . . . . . . . . . . . . . . 18 ((inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+ ∧ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
428159, 423, 427syl2anc 691 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
429428expl 646 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
430429exlimdv 1848 . . . . . . . . . . . . . . 15 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → (∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
431430expimpd 627 . . . . . . . . . . . . . 14 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → (( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
432103, 431sylan2 490 . . . . . . . . . . . . 13 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)) → (( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
433432rexlimdva 3013 . . . . . . . . . . . 12 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
434102, 433syld 46 . . . . . . . . . . 11 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
43515, 434syl5 33 . . . . . . . . . 10 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (((𝑑 / 2) ∈ ℝ+ ∧ ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
436435exp4b 630 . . . . . . . . 9 ((𝜑𝑓:𝑋𝑌) → (𝑑 ∈ ℝ+ → ((𝑑 / 2) ∈ ℝ+ → (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))))
4379, 436mpdi 44 . . . . . . . 8 ((𝜑𝑓:𝑋𝑌) → (𝑑 ∈ ℝ+ → (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
438437ralrimiv 2948 . . . . . . 7 ((𝜑𝑓:𝑋𝑌) → ∀𝑑 ∈ ℝ+ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
439 r19.21v 2943 . . . . . . 7 (∀𝑑 ∈ ℝ+ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) ↔ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
440438, 439sylib 207 . . . . . 6 ((𝜑𝑓:𝑋𝑌) → (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
4418, 440impbid2 215 . . . . 5 ((𝜑𝑓:𝑋𝑌) → (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
442 ralcom 3079 . . . . 5 (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
443441, 442syl6bb 275 . . . 4 ((𝜑𝑓:𝑋𝑌) → (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
444443pm5.32da 671 . . 3 (𝜑 → ((𝑓:𝑋𝑌 ∧ ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
445 eqid 2610 . . . 4 (metUnif‘𝐶) = (metUnif‘𝐶)
446 eqid 2610 . . . 4 (metUnif‘𝐷) = (metUnif‘𝐷)
447 heicant.y . . . 4 (𝜑𝑌 ≠ ∅)
448 xmetpsmet 21963 . . . . 5 (𝐶 ∈ (∞Met‘𝑋) → 𝐶 ∈ (PsMet‘𝑋))
44918, 448syl 17 . . . 4 (𝜑𝐶 ∈ (PsMet‘𝑋))
450 xmetpsmet 21963 . . . . 5 (𝐷 ∈ (∞Met‘𝑌) → 𝐷 ∈ (PsMet‘𝑌))
451329, 450syl 17 . . . 4 (𝜑𝐷 ∈ (PsMet‘𝑌))
452445, 446, 129, 447, 449, 451metucn 22186 . . 3 (𝜑 → (𝑓 ∈ ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
453 eqid 2610 . . . . 5 (MetOpen‘𝐷) = (MetOpen‘𝐷)
45423, 453metcn 22158 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) → (𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
45518, 329, 454syl2anc 691 . . 3 (𝜑 → (𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
456444, 452, 4553bitr4d 299 . 2 (𝜑 → (𝑓 ∈ ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) ↔ 𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷))))
457456eqrdv 2608 1 (𝜑 → ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) = ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wex 1695  wcel 1977  wne 2780  wral 2896  wrex 2897  cin 3539  wss 3540  c0 3874  𝒫 cpw 4108  cop 4131   cuni 4372   class class class wbr 4583   Or wor 4958   × cxp 5036  dom cdm 5038  ran crn 5039  Rel wrel 5043  Fun wfun 5798   Fn wfn 5799  wf 5800  cfv 5804  (class class class)co 6549  1st c1st 7057  2nd c2nd 7058  cen 7838  Fincfn 7841  infcinf 8230  cr 9814  0cc0 9815   + caddc 9818  *cxr 9952   < clt 9953  cle 9954   / cdiv 10563  2c2 10947  +crp 11708   +𝑒 cxad 11820  PsMetcpsmet 19551  ∞Metcxmt 19552  ballcbl 19554  MetOpencmopn 19557  metUnifcmetu 19558   Cn ccn 20838  Compccmp 20999   Cnucucn 21889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ico 12052  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-metu 19566  df-top 20521  df-bases 20522  df-topon 20523  df-cn 20841  df-cnp 20842  df-cmp 21000  df-fil 21460  df-ust 21814  df-ucn 21890
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator