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 37976
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 5089 . . . . . . . . . . 11 (𝑑 = 𝑦 → (((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑 ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
21imbi2d 340 . . . . . . . . . 10 (𝑑 = 𝑦 → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
322ralbidv 3201 . . . . . . . . 9 (𝑑 = 𝑦 → (∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
43rexbidv 3161 . . . . . . . 8 (𝑑 = 𝑦 → (∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
54cbvralvw 3215 . . . . . . 7 (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
6 r19.12 3286 . . . . . . . 8 (∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
76ralimi 3074 . . . . . . 7 (∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
85, 7sylbi 217 . . . . . 6 (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) → ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
9 rphalfcl 12971 . . . . . . . . 9 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ+)
10 breq2 5089 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑑 / 2) → (((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦 ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
1110imbi2d 340 . . . . . . . . . . . . . . 15 (𝑦 = (𝑑 / 2) → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1211ralbidv 3160 . . . . . . . . . . . . . 14 (𝑦 = (𝑑 / 2) → (∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1312rexbidv 3161 . . . . . . . . . . . . 13 (𝑦 = (𝑑 / 2) → (∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1413ralbidv 3160 . . . . . . . . . . . 12 (𝑦 = (𝑑 / 2) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
1514rspcva 3562 . . . . . . . . . . 11 (((𝑑 / 2) ∈ ℝ+ ∧ ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)) → ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
16 heicant.j . . . . . . . . . . . . . . 15 (𝜑 → (MetOpen‘𝐶) ∈ Comp)
1716ad3antrrr 731 . . . . . . . . . . . . . 14 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (MetOpen‘𝐶) ∈ Comp)
18 heicant.c . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐶 ∈ (∞Met‘𝑋))
1918ad2antrr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → 𝐶 ∈ (∞Met‘𝑋))
2019anim1i 616 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) → (𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋))
21 rphalfcl 12971 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → (𝑧 / 2) ∈ ℝ+)
2221rpxrd 12987 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ℝ+ → (𝑧 / 2) ∈ ℝ*)
23 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . 23 (MetOpen‘𝐶) = (MetOpen‘𝐶)
2423blopn 24465 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋 ∧ (𝑧 / 2) ∈ ℝ*) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
25243expa 1119 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧 / 2) ∈ ℝ*) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2620, 22, 25syl2an 597 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2726adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶))
2821rpgt0d 12989 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → 0 < (𝑧 / 2))
2922, 28jca 511 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ℝ+ → ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2)))
30 xblcntr 24376 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋 ∧ ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
31303expa 1119 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ ((𝑧 / 2) ∈ ℝ* ∧ 0 < (𝑧 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
3220, 29, 31syl2an 597 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
3332adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → 𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)))
34 opelxpi 5668 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑋 ∧ (𝑧 / 2) ∈ ℝ+) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
3521, 34sylan2 594 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑋𝑧 ∈ ℝ+) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
3635ad4ant23 754 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+))
37 rpcn 12953 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ ℝ+𝑧 ∈ ℂ)
38372halvesd 12423 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℝ+ → ((𝑧 / 2) + (𝑧 / 2)) = 𝑧)
3938breq2d 5097 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ℝ+ → ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) ↔ (𝑥𝐶𝑐) < 𝑧))
4039imbi1d 341 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ℝ+ → (((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
4140ralbidv 3160 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ ℝ+ → (∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
42 oveq2 7375 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑤 → (𝑥𝐶𝑐) = (𝑥𝐶𝑤))
4342breq1d 5095 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑤 → ((𝑥𝐶𝑐) < 𝑧 ↔ (𝑥𝐶𝑤) < 𝑧))
44 fveq2 6840 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 = 𝑤 → (𝑓𝑐) = (𝑓𝑤))
4544oveq2d 7383 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑤 → ((𝑓𝑥)𝐷(𝑓𝑐)) = ((𝑓𝑥)𝐷(𝑓𝑤)))
4645breq1d 5095 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑤 → (((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
4743, 46imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑤 → (((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
4847cbvralvw 3215 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑐𝑋 ((𝑥𝐶𝑐) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)))
4941, 48bitrdi 287 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ℝ+ → (∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))))
5049biimpar 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 ∈ ℝ+ ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
5150adantll 715 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
52 vex 3433 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥 ∈ V
53 ovex 7400 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 / 2) ∈ V
5452, 53op1std 7952 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (1st𝑝) = 𝑥)
5552, 53op2ndd 7953 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (2nd𝑝) = (𝑧 / 2))
5654, 55oveq12d 7385 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((1st𝑝)(ball‘𝐶)(2nd𝑝)) = (𝑥(ball‘𝐶)(𝑧 / 2)))
5756eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . 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 7382 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((1st𝑝)𝐶𝑐) = (𝑥𝐶𝑐))
6055, 55oveq12d 7385 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((2nd𝑝) + (2nd𝑝)) = ((𝑧 / 2) + (𝑧 / 2)))
6159, 60breq12d 5098 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) ↔ (𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2))))
6254fveq2d 6844 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (𝑓‘(1st𝑝)) = (𝑓𝑥))
6362oveq1d 7382 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) = ((𝑓𝑥)𝐷(𝑓𝑐)))
6463breq1d 5095 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2)))
6561, 64imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → ((((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
6665ralbidv 3160 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
6758, 66bitr3d 281 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = ⟨𝑥, (𝑧 / 2)⟩ → (((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))))
6867rspcev 3564 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑥, (𝑧 / 2)⟩ ∈ (𝑋 × ℝ+) ∧ ∀𝑐𝑋 ((𝑥𝐶𝑐) < ((𝑧 / 2) + (𝑧 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑐)) < (𝑑 / 2))) → ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))
6936, 51, 68syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))
70 eleq2 2825 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (𝑥𝑏𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2))))
71 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ↔ (𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝))))
7271anbi1d 632 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → ((𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7372rexbidv 3161 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → (∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7470, 73anbi12d 633 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = (𝑥(ball‘𝐶)(𝑧 / 2)) → ((𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ (𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)) ∧ ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
7574rspcev 3564 . . . . . . . . . . . . . . . . . . 19 (((𝑥(ball‘𝐶)(𝑧 / 2)) ∈ (MetOpen‘𝐶) ∧ (𝑥 ∈ (𝑥(ball‘𝐶)(𝑧 / 2)) ∧ ∃𝑝 ∈ (𝑋 × ℝ+)((𝑥(ball‘𝐶)(𝑧 / 2)) = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7627, 33, 69, 75syl12anc 837 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) ∧ 𝑧 ∈ ℝ+) ∧ ∀𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
7776rexlimdva2 3140 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑥𝑋) → (∃𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
7877ralimdva 3149 . . . . . . . . . . . . . . . 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 24406 . . . . . . . . . . . . . . . . . 18 (𝐶 ∈ (∞Met‘𝑋) → 𝑋 = (MetOpen‘𝐶))
8118, 80syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 = (MetOpen‘𝐶))
8281raleqdv 3295 . . . . . . . . . . . . . . . 16 (𝜑 → (∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
8382ad3antrrr 731 . . . . . . . . . . . . . . 15 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → (∀𝑥𝑋𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ↔ ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
8479, 83mpbid 232 . . . . . . . . . . . . . 14 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
85 eqid 2736 . . . . . . . . . . . . . . 15 (MetOpen‘𝐶) = (MetOpen‘𝐶)
86 fveq2 6840 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (1st𝑝) = (1st ‘(𝑔𝑏)))
87 fveq2 6840 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (2nd𝑝) = (2nd ‘(𝑔𝑏)))
8886, 87oveq12d 7385 . . . . . . . . . . . . . . . . 17 (𝑝 = (𝑔𝑏) → ((1st𝑝)(ball‘𝐶)(2nd𝑝)) = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))))
8988eqeq2d 2747 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑔𝑏) → (𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ↔ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))))
9086oveq1d 7382 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((1st𝑝)𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑐))
9187, 87oveq12d 7385 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((2nd𝑝) + (2nd𝑝)) = ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
9290, 91breq12d 5098 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) ↔ ((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
9386fveq2d 6844 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = (𝑔𝑏) → (𝑓‘(1st𝑝)) = (𝑓‘(1st ‘(𝑔𝑏))))
9493oveq1d 7382 . . . . . . . . . . . . . . . . . . 19 (𝑝 = (𝑔𝑏) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)))
9594breq1d 5095 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑔𝑏) → (((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))
9692, 95imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑝 = (𝑔𝑏) → ((((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
9796ralbidv 3160 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑔𝑏) → (∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
9889, 97anbi12d 633 . . . . . . . . . . . . . . 15 (𝑝 = (𝑔𝑏) → ((𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))) ↔ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))))
9985, 98cmpcovf 23356 . . . . . . . . . . . . . 14 (((MetOpen‘𝐶) ∈ Comp ∧ ∀𝑥 (MetOpen‘𝐶)∃𝑏 ∈ (MetOpen‘𝐶)(𝑥𝑏 ∧ ∃𝑝 ∈ (𝑋 × ℝ+)(𝑏 = ((1st𝑝)(ball‘𝐶)(2nd𝑝)) ∧ ∀𝑐𝑋 (((1st𝑝)𝐶𝑐) < ((2nd𝑝) + (2nd𝑝)) → ((𝑓‘(1st𝑝))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
10017, 84, 99syl2anc 585 . . . . . . . . . . . . 13 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ ∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2))) → ∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))))
101100ex 412 . . . . . . . . . . . 12 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → (∀𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < (𝑑 / 2)) → ∃𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))))))
102 elinel2 4142 . . . . . . . . . . . . . 14 (𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin) → 𝑠 ∈ Fin)
103 simpll 767 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) → 𝜑)
104103anim1i 616 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → (𝜑𝑠 ∈ Fin))
105 frn 6675 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran 𝑔 ⊆ (𝑋 × ℝ+))
106 rnss 5894 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ⊆ (𝑋 × ℝ+) → ran ran 𝑔 ⊆ ran (𝑋 × ℝ+))
107105, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ran (𝑋 × ℝ+))
108 rnxpss 6136 . . . . . . . . . . . . . . . . . . . . . . 23 ran (𝑋 × ℝ+) ⊆ ℝ+
109107, 108sstrdi 3934 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ℝ+)
110109adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ⊆ ℝ+)
111 simplr 769 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → 𝑠 ∈ Fin)
112 ffun 6671 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔:𝑠⟶(𝑋 × ℝ+) → Fun 𝑔)
113 vex 3433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑔 ∈ V
114113fundmen 8978 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun 𝑔 → dom 𝑔𝑔)
115114ensymd 8952 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Fun 𝑔𝑔 ≈ dom 𝑔)
116112, 115syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔 ≈ dom 𝑔)
117 fdm 6677 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → dom 𝑔 = 𝑠)
118116, 117breqtrd 5111 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔𝑠)
119 enfii 9120 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ Fin ∧ 𝑔𝑠) → 𝑔 ∈ Fin)
120118, 119sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ Fin ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑔 ∈ Fin)
121 rnfi 9250 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔 ∈ Fin → ran 𝑔 ∈ Fin)
122 rnfi 9250 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ∈ Fin → ran ran 𝑔 ∈ Fin)
123120, 121, 1223syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ Fin ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ∈ Fin)
124111, 123sylan 581 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ∈ Fin)
125117adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → dom 𝑔 = 𝑠)
126 eqtr 2756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → 𝑋 = 𝑠)
12781, 126sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑋 = 𝑠)
128 heicant.x . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑋 ≠ ∅)
129128adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑋 ≠ ∅)
130127, 129eqnetrrd 3000 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑠 ≠ ∅)
131 unieq 4861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑠 = ∅ → 𝑠 = ∅)
132 uni0 4878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ∅ = ∅
133131, 132eqtrdi 2787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 = ∅ → 𝑠 = ∅)
134133necon3i 2964 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( 𝑠 ≠ ∅ → 𝑠 ≠ ∅)
135130, 134syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 (MetOpen‘𝐶) = 𝑠) → 𝑠 ≠ ∅)
136135adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑠 ≠ ∅)
137125, 136eqnetrd 2999 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → dom 𝑔 ≠ ∅)
138 dm0rn0 5879 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑔 = ∅ ↔ ran 𝑔 = ∅)
139138necon3bii 2984 . . . . . . . . . . . . . . . . . . . . . . . . 25 (dom 𝑔 ≠ ∅ ↔ ran 𝑔 ≠ ∅)
140137, 139sylib 218 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran 𝑔 ≠ ∅)
141 relxp 5649 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Rel (𝑋 × ℝ+)
142 relss 5738 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ran 𝑔 ⊆ (𝑋 × ℝ+) → (Rel (𝑋 × ℝ+) → Rel ran 𝑔))
143105, 141, 142mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:𝑠⟶(𝑋 × ℝ+) → Rel ran 𝑔)
144 relrn0 5928 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Rel ran 𝑔 → (ran 𝑔 = ∅ ↔ ran ran 𝑔 = ∅))
145144necon3bid 2976 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Rel ran 𝑔 → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
146143, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔:𝑠⟶(𝑋 × ℝ+) → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
147146adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (ran 𝑔 ≠ ∅ ↔ ran ran 𝑔 ≠ ∅))
148140, 147mpbid 232 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ≠ ∅)
149148adantllr 720 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ≠ ∅)
150 rpssre 12950 . . . . . . . . . . . . . . . . . . . . . . 23 + ⊆ ℝ
151110, 150sstrdi 3934 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → ran ran 𝑔 ⊆ ℝ)
152 ltso 11226 . . . . . . . . . . . . . . . . . . . . . . 23 < Or ℝ
153 fiinfcl 9416 . . . . . . . . . . . . . . . . . . . . . . 23 (( < Or ℝ ∧ (ran ran 𝑔 ∈ Fin ∧ ran ran 𝑔 ≠ ∅ ∧ ran ran 𝑔 ⊆ ℝ)) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
154152, 153mpan 691 . . . . . . . . . . . . . . . . . . . . . 22 ((ran ran 𝑔 ∈ Fin ∧ ran ran 𝑔 ≠ ∅ ∧ ran ran 𝑔 ⊆ ℝ) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
155124, 149, 151, 154syl3anc 1374 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ran ran 𝑔)
156110, 155sseldd 3922 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
157104, 156sylanl1 681 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
158157adantr 480 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+)
15981ad3antrrr 731 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → 𝑋 = (MetOpen‘𝐶))
160159anim1i 616 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠))
161160ad2antrr 727 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠))
162 simpl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑋𝑤𝑋) → 𝑥𝑋)
163126eleq2d 2822 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑥𝑋𝑥 𝑠))
164 eluni2 4854 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 𝑠 ↔ ∃𝑏𝑠 𝑥𝑏)
165163, 164bitrdi 287 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) → (𝑥𝑋 ↔ ∃𝑏𝑠 𝑥𝑏))
166165biimpa 476 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋 = (MetOpen‘𝐶) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑥𝑋) → ∃𝑏𝑠 𝑥𝑏)
167161, 162, 166syl2an 597 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋)) → ∃𝑏𝑠 𝑥𝑏)
168 nfv 1916 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏(((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+))
169 nfra1 3261 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))
170168, 169nfan 1901 . . . . . . . . . . . . . . . . . . . . . 22 𝑏((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
171 nfv 1916 . . . . . . . . . . . . . . . . . . . . . 22 𝑏(𝑥𝑋𝑤𝑋)
172170, 171nfan 1901 . . . . . . . . . . . . . . . . . . . . 21 𝑏(((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋))
173 nfv 1916 . . . . . . . . . . . . . . . . . . . . 21 𝑏((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)
174 rspa 3226 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ 𝑏𝑠) → (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))
175 oveq2 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑥 → ((1st ‘(𝑔𝑏))𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑥))
176175breq1d 5095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑥 → (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ↔ ((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
177 fveq2 6840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑐 = 𝑥 → (𝑓𝑐) = (𝑓𝑥))
178177oveq2d 7383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑥 → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
179178breq1d 5095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑥 → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)))
180176, 179imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑥 → ((((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2))))
181180rspcva 3562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑥𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)))
182 oveq2 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑤 → ((1st ‘(𝑔𝑏))𝐶𝑐) = ((1st ‘(𝑔𝑏))𝐶𝑤))
183182breq1d 5095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ↔ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
18444oveq2d 7383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑤 → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
185184breq1d 5095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2) ↔ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)))
186183, 185imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑤 → ((((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)) ↔ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
187186rspcva 3562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑤𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)))
188181, 187anim12i 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑥𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ (𝑤𝑋 ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
189188anandirs 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥𝑋𝑤𝑋) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
190 anim12 809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
191189, 190syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥𝑋𝑤𝑋) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
192191adantrl 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥𝑋𝑤𝑋) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
193192ad4ant23 754 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑏𝑠𝑥𝑏)) → ((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))))
194 simpll 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → ((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+))
195194anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)))
196195anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)))
197109, 150sstrdi 3934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑔:𝑠⟶(𝑋 × ℝ+) → ran ran 𝑔 ⊆ ℝ)
198197adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ran ran 𝑔 ⊆ ℝ)
199 0re 11146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 ∈ ℝ
200 rpge0 12956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦 ∈ ℝ+ → 0 ≤ 𝑦)
201200rgen 3053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 𝑦 ∈ ℝ+ 0 ≤ 𝑦
202 ssralv 3990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (ran ran 𝑔 ⊆ ℝ+ → (∀𝑦 ∈ ℝ+ 0 ≤ 𝑦 → ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦))
203109, 201, 202mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔:𝑠⟶(𝑋 × ℝ+) → ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦)
204 breq1 5088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑥 = 0 → (𝑥𝑦 ↔ 0 ≤ 𝑦))
205204ralbidv 3160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑥 = 0 → (∀𝑦 ∈ ran ran 𝑔 𝑥𝑦 ↔ ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦))
206205rspcev 3564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((0 ∈ ℝ ∧ ∀𝑦 ∈ ran ran 𝑔0 ≤ 𝑦) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
207199, 203, 206sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑔:𝑠⟶(𝑋 × ℝ+) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
208207adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦)
209143adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → Rel ran 𝑔)
210 ffn 6668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔:𝑠⟶(𝑋 × ℝ+) → 𝑔 Fn 𝑠)
211 fnfvelrn 7032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔 Fn 𝑠𝑏𝑠) → (𝑔𝑏) ∈ ran 𝑔)
212210, 211sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ ran 𝑔)
213 2ndrn 7994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((Rel ran 𝑔 ∧ (𝑔𝑏) ∈ ran 𝑔) → (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔)
214209, 212, 213syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔)
215 infrelb 12141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((ran ran 𝑔 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦 ∧ (2nd ‘(𝑔𝑏)) ∈ ran ran 𝑔) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
216198, 208, 214, 215syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
217216adantll 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
218217ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏)))
21918ad3antrrr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝐶 ∈ (∞Met‘𝑋))
220 xmetcl 24296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋𝑤𝑋) → (𝑥𝐶𝑤) ∈ ℝ*)
2212203expb 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥𝑋𝑤𝑋)) → (𝑥𝐶𝑤) ∈ ℝ*)
222219, 221sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑥𝐶𝑤) ∈ ℝ*)
223222adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (𝑥𝐶𝑤) ∈ ℝ*)
224 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → 𝑔:𝑠⟶(𝑋 × ℝ+))
225 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑏𝑠𝑥𝑏) → 𝑏𝑠)
226214ne0d 4282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → ran ran 𝑔 ≠ ∅)
227 infrecl 12138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((ran ran 𝑔 ⊆ ℝ ∧ ran ran 𝑔 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ran 𝑔 𝑥𝑦) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ)
228198, 226, 208, 227syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ)
229228rexrd 11195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ*)
230224, 225, 229syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → inf(ran ran 𝑔, ℝ, < ) ∈ ℝ*)
231 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑔:𝑠⟶(𝑋 × ℝ+))
232231ffvelcdmda 7036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
233 xp2nd 7975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔𝑏) ∈ (𝑋 × ℝ+) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
234232, 233syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
235234rpxrd 12987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
236235ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
237 xrltletr 13108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑥𝐶𝑤) ∈ ℝ* ∧ inf(ran ran 𝑔, ℝ, < ) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → (((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) ∧ inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
238223, 230, 236, 237syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) ∧ inf(ran ran 𝑔, ℝ, < ) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
239218, 238mpan2d 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
240239adantlr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))))
24118ad6antr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝐶 ∈ (∞Met‘𝑋))
242 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → 𝑔:𝑠⟶(𝑋 × ℝ+))
243 ffvelcdm 7033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
244 xp1st 7974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑔𝑏) ∈ (𝑋 × ℝ+) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
245243, 244syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
246242, 225, 245syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
247 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑥𝑋𝑤𝑋) → 𝑤𝑋)
248247ad3antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝑤𝑋)
249 xmetcl 24296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑤𝑋) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
250241, 246, 248, 249syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
251250adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) ∈ ℝ*)
252243, 233syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
253224, 252sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
254253ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ+)
255254rpred 12986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
256162ad3antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → 𝑥𝑋)
257 xmetcl 24296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑥𝑋) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
258241, 246, 256, 257syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
259252rpxrd 12987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
260242, 225, 259syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
261 eleq2 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) → (𝑥𝑏𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))))
26218ad5antr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝐶 ∈ (∞Met‘𝑋))
263224, 245sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
264253rpxrd 12987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ*)
265 elbl 24353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋 ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → (𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
266262, 263, 264, 265syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑥 ∈ ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
267261, 266sylan9bbr 510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → (𝑥𝑏 ↔ (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
268267biimpd 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) → (𝑥𝑏 → (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
269268an32s 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ 𝑏𝑠) → (𝑥𝑏 → (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))))
270269impr 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (𝑥𝑋 ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏))))
271270simprd 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) < (2nd ‘(𝑔𝑏)))
272258, 260, 271xrltled 13101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))
273224ffvelcdmda 7036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑔𝑏) ∈ (𝑋 × ℝ+))
274273, 244syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (1st ‘(𝑔𝑏)) ∈ 𝑋)
275 simplrl 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝑥𝑋)
276262, 274, 275, 257syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ*)
277 xmetge0 24309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐶 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔𝑏)) ∈ 𝑋𝑥𝑋) → 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥))
278262, 274, 275, 277syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥))
279 xrrege0 13126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) ∧ (0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥) ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
280279an4s 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥)) ∧ ((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏)))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
281280ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ* ∧ 0 ≤ ((1st ‘(𝑔𝑏))𝐶𝑥)) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
282276, 278, 281syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
283282ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((2nd ‘(𝑔𝑏)) ∈ ℝ ∧ ((1st ‘(𝑔𝑏))𝐶𝑥) ≤ (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ))
284255, 272, 283mp2and 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
285284adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ)
286 xrltle 13100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ*) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))))
287223, 236, 286syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))))
288 xmetge0 24309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋𝑤𝑋) → 0 ≤ (𝑥𝐶𝑤))
2892883expb 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑥𝑋𝑤𝑋)) → 0 ≤ (𝑥𝐶𝑤))
290219, 289sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → 0 ≤ (𝑥𝐶𝑤))
291290adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → 0 ≤ (𝑥𝐶𝑤))
292234rpred 12986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
293292ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
294 xrrege0 13126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) ∧ (0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏)))) → (𝑥𝐶𝑤) ∈ ℝ)
295294ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑥𝐶𝑤) ∈ ℝ* ∧ (2nd ‘(𝑔𝑏)) ∈ ℝ) → ((0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ))
296223, 293, 295syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((0 ≤ (𝑥𝐶𝑤) ∧ (𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ))
297291, 296mpand 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) ≤ (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
298287, 297syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
299298adantlr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (𝑥𝐶𝑤) ∈ ℝ))
300299imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (𝑥𝐶𝑤) ∈ ℝ)
301285, 300readdcld 11174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) ∈ ℝ)
302301rexrd 11195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) ∈ ℝ*)
303254, 254rpaddcld 13001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ+)
304303rpxrd 12987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ*)
305304adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∈ ℝ*)
306 xmettri 24316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐶 ∈ (∞Met‘𝑋) ∧ ((1st ‘(𝑔𝑏)) ∈ 𝑋𝑤𝑋𝑥𝑋)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
307241, 246, 248, 256, 306syl13anc 1375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
308307adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) ≤ (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)))
309 rexadd 13184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((1st ‘(𝑔𝑏))𝐶𝑥) ∈ ℝ ∧ (𝑥𝐶𝑤) ∈ ℝ) → (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)) = (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)))
310285, 300, 309syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) +𝑒 (𝑥𝐶𝑤)) = (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)))
311308, 310breqtrd 5111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → (((1st ‘(𝑔𝑏))𝐶𝑥) + (𝑥𝐶𝑤)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
316251, 302, 305, 311, 315xrlelttrd 13111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏))) → ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
317316ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))))
318252rpred 12986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) ∈ ℝ)
319318, 252ltaddrpd 13019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ 𝑏𝑠) → (2nd ‘(𝑔𝑏)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
320242, 225, 319syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (2nd ‘(𝑔𝑏)) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
321258, 260, 304, 271, 320xrlttrd 13110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))
322317, 321jctild 525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < (2nd ‘(𝑔𝑏)) → (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))))
323240, 322syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → (((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))))))
324 simpll 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → (𝜑𝑓:𝑋𝑌))
325 heicant.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑𝐷 ∈ (∞Met‘𝑌))
326 ffvelcdm 7033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑓:𝑋𝑌𝑥𝑋) → (𝑓𝑥) ∈ 𝑌)
327 ffvelcdm 7033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑓:𝑋𝑌𝑤𝑋) → (𝑓𝑤) ∈ 𝑌)
328326, 327anim12dan 620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑋𝑌 ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌))
329 xmetcl 24296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
3303293expb 1121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐷 ∈ (∞Met‘𝑌) ∧ ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
331325, 328, 330syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑 ∧ (𝑓:𝑋𝑌 ∧ (𝑥𝑋𝑤𝑋))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
332331anassrs 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑓:𝑋𝑌) ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
333324, 332sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
334333ad3antrrr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ∈ ℝ*)
335325ad5antr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝐷 ∈ (∞Met‘𝑌))
336 simp-5r 786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 𝑓:𝑋𝑌)
337336, 274ffvelcdmd 7037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌)
338 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) → 𝑓:𝑋𝑌)
339338ffvelcdmda 7036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑥𝑋) → (𝑓𝑥) ∈ 𝑌)
340339adantrr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑓𝑥) ∈ 𝑌)
341340adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓𝑥) ∈ 𝑌)
342 xmetcl 24296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑥) ∈ 𝑌) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ*)
343335, 337, 341, 342syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ*)
3449rpxrd 12987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ*)
345344ad4antlr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑑 / 2) ∈ ℝ*)
346 xrltle 13100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ*) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)))
347343, 345, 346syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)))
348 xmetge0 24309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑥) ∈ 𝑌) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
349335, 337, 341, 348syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
3509rpred 12986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑑 ∈ ℝ+ → (𝑑 / 2) ∈ ℝ)
351350ad4antlr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑑 / 2) ∈ ℝ)
352 xrrege0 13126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) ∧ (0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ)
353352ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
354343, 351, 353syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
355349, 354mpand 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ≤ (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
356347, 355syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
357356ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ))
358357imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ)
359338ffvelcdmda 7036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ 𝑤𝑋) → (𝑓𝑤) ∈ 𝑌)
360359adantrl 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) → (𝑓𝑤) ∈ 𝑌)
361360adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (𝑓𝑤) ∈ 𝑌)
362 xmetcl 24296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ*)
363335, 337, 361, 362syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ*)
364 xrltle 13100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ*) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)))
365363, 345, 364syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)))
366 xmetge0 24309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
367335, 337, 361, 366syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → 0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)))
368 xrrege0 13126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) ∧ (0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ)
369368ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ* ∧ (𝑑 / 2) ∈ ℝ) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
370363, 351, 369syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((0 ≤ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
371367, 370mpand 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ≤ (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
372365, 371syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
373372ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ))
374373imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ)
375 readdcl 11121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
376358, 374, 375syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
377376anandis 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ)
378377rexrd 11195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) ∈ ℝ*)
379 rpxr 12952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 ∈ ℝ+𝑑 ∈ ℝ*)
380379ad6antlr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → 𝑑 ∈ ℝ*)
381 xmettri 24316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐷 ∈ (∞Met‘𝑌) ∧ ((𝑓𝑥) ∈ 𝑌 ∧ (𝑓𝑤) ∈ 𝑌 ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
382335, 341, 361, 337, 381syl13anc 1375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
383382ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
384383adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
385 xmetsym 24312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐷 ∈ (∞Met‘𝑌) ∧ (𝑓𝑥) ∈ 𝑌 ∧ (𝑓‘(1st ‘(𝑔𝑏))) ∈ 𝑌) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
386335, 341, 337, 385syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
387386ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
388387adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) = ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)))
389388oveq1d 7382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
390 rexadd 13184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
391358, 374, 390syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2)) ∧ (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
392391anandis 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
393389, 392eqtrd 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓𝑥)𝐷(𝑓‘(1st ‘(𝑔𝑏)))) +𝑒 ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) = (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
394384, 393breqtrd 5111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) ≤ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))))
395 lt2add 11635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) ∧ ((𝑑 / 2) ∈ ℝ ∧ (𝑑 / 2) ∈ ℝ)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2))))
396395expcom 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑑 / 2) ∈ ℝ ∧ (𝑑 / 2) ∈ ℝ) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))))
397351, 351, 396syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) ∈ ℝ ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) ∈ ℝ) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))))
398356, 372, 397syl2and 609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))))
399398pm2.43d 53 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏𝑠) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2))))
400399ad2ant2r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2))))
401400imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < ((𝑑 / 2) + (𝑑 / 2)))
402 rpcn 12953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑑 ∈ ℝ+𝑑 ∈ ℂ)
4034022halvesd 12423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 ∈ ℝ+ → ((𝑑 / 2) + (𝑑 / 2)) = 𝑑)
404403ad6antlr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑑 / 2) + (𝑑 / 2)) = 𝑑)
405401, 404breqtrd 5111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) + ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤))) < 𝑑)
406334, 378, 380, 394, 405xrlelttrd 13111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) ∧ (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)
407406ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → ((((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2)) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
408323, 407imim12d 81 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
409196, 408sylanl1 681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ 𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏)))) ∧ (𝑏𝑠𝑥𝑏)) → (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
410409adantlrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑏𝑠𝑥𝑏)) → (((((1st ‘(𝑔𝑏))𝐶𝑥) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) ∧ ((1st ‘(𝑔𝑏))𝐶𝑤) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏)))) → (((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑥)) < (𝑑 / 2) ∧ ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑤)) < (𝑑 / 2))) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
411193, 410mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑏𝑠𝑥𝑏)) → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
412411exp32 420 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
413174, 412sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ (∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))) ∧ 𝑏𝑠)) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
414413expr 456 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑏𝑠 → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))))
415414pm2.43d 53 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ (𝑥𝑋𝑤𝑋)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
416415an32s 653 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) ∧ (𝑥𝑋𝑤𝑋)) → (𝑏𝑠 → (𝑥𝑏 → ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
417172, 173, 416rexlimd 3244 . . . . . . . . . . . . . . . . . . . 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 3180 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
420 breq2 5089 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → ((𝑥𝐶𝑤) < 𝑧 ↔ (𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < )))
421420imbi1d 341 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → (((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
4224212ralbidv 3201 . . . . . . . . . . . . . . . . . . 19 (𝑧 = inf(ran ran 𝑔, ℝ, < ) → (∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
423422rspcev 3564 . . . . . . . . . . . . . . . . . 18 ((inf(ran ran 𝑔, ℝ, < ) ∈ ℝ+ ∧ ∀𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < inf(ran ran 𝑔, ℝ, < ) → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
424158, 419, 423syl2anc 585 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) ∧ 𝑔:𝑠⟶(𝑋 × ℝ+)) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))
425424expl 457 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → ((𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
426425exlimdv 1935 . . . . . . . . . . . . . . 15 (((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) ∧ (MetOpen‘𝐶) = 𝑠) → (∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2)))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
427426expimpd 453 . . . . . . . . . . . . . 14 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ Fin) → (( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
428102, 427sylan2 594 . . . . . . . . . . . . 13 ((((𝜑𝑓:𝑋𝑌) ∧ 𝑑 ∈ ℝ+) ∧ 𝑠 ∈ (𝒫 (MetOpen‘𝐶) ∩ Fin)) → (( (MetOpen‘𝐶) = 𝑠 ∧ ∃𝑔(𝑔:𝑠⟶(𝑋 × ℝ+) ∧ ∀𝑏𝑠 (𝑏 = ((1st ‘(𝑔𝑏))(ball‘𝐶)(2nd ‘(𝑔𝑏))) ∧ ∀𝑐𝑋 (((1st ‘(𝑔𝑏))𝐶𝑐) < ((2nd ‘(𝑔𝑏)) + (2nd ‘(𝑔𝑏))) → ((𝑓‘(1st ‘(𝑔𝑏)))𝐷(𝑓𝑐)) < (𝑑 / 2))))) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
429428rexlimdva 3138 . . . . . . . . . . . 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 3128 . . . . . . 7 ((𝜑𝑓:𝑋𝑌) → ∀𝑑 ∈ ℝ+ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
435 r19.21v 3162 . . . . . . 7 (∀𝑑 ∈ ℝ+ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∃𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) ↔ (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
436434, 435sylib 218 . . . . . 6 ((𝜑𝑓:𝑋𝑌) → (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) → ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)))
4378, 436impbid2 226 . . . . 5 ((𝜑𝑓:𝑋𝑌) → (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
438 ralcom 3265 . . . . 5 (∀𝑦 ∈ ℝ+𝑥𝑋𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦) ↔ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))
439437, 438bitrdi 287 . . . 4 ((𝜑𝑓:𝑋𝑌) → (∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑) ↔ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦)))
440439pm5.32da 579 . . 3 (𝜑 → ((𝑓:𝑋𝑌 ∧ ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
441 eqid 2736 . . . 4 (metUnif‘𝐶) = (metUnif‘𝐶)
442 eqid 2736 . . . 4 (metUnif‘𝐷) = (metUnif‘𝐷)
443 heicant.y . . . 4 (𝜑𝑌 ≠ ∅)
444 xmetpsmet 24313 . . . . 5 (𝐶 ∈ (∞Met‘𝑋) → 𝐶 ∈ (PsMet‘𝑋))
44518, 444syl 17 . . . 4 (𝜑𝐶 ∈ (PsMet‘𝑋))
446 xmetpsmet 24313 . . . . 5 (𝐷 ∈ (∞Met‘𝑌) → 𝐷 ∈ (PsMet‘𝑌))
447325, 446syl 17 . . . 4 (𝜑𝐷 ∈ (PsMet‘𝑌))
448441, 442, 128, 443, 445, 447metucn 24536 . . 3 (𝜑 → (𝑓 ∈ ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑑 ∈ ℝ+𝑧 ∈ ℝ+𝑥𝑋𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑑))))
449 eqid 2736 . . . . 5 (MetOpen‘𝐷) = (MetOpen‘𝐷)
45023, 449metcn 24508 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) → (𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
45118, 325, 450syl2anc 585 . . 3 (𝜑 → (𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝑓𝑥)𝐷(𝑓𝑤)) < 𝑦))))
452440, 448, 4513bitr4d 311 . 2 (𝜑 → (𝑓 ∈ ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) ↔ 𝑓 ∈ ((MetOpen‘𝐶) Cn (MetOpen‘𝐷))))
453452eqrdv 2734 1 (𝜑 → ((metUnif‘𝐶) Cnu(metUnif‘𝐷)) = ((MetOpen‘𝐶) Cn (MetOpen‘𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1542  wex 1781  wcel 2114  wne 2932  wral 3051  wrex 3061  cin 3888  wss 3889  c0 4273  𝒫 cpw 4541  cop 4573   cuni 4850   class class class wbr 5085   Or wor 5538   × cxp 5629  dom cdm 5631  ran crn 5632  Rel wrel 5636  Fun wfun 6492   Fn wfn 6493  wf 6494  cfv 6498  (class class class)co 7367  1st c1st 7940  2nd c2nd 7941  cen 8890  Fincfn 8893  infcinf 9354  cr 11037  0cc0 11038   + caddc 11041  *cxr 11178   < clt 11179  cle 11180   / cdiv 11807  2c2 12236  +crp 12942   +𝑒 cxad 13061  PsMetcpsmet 21336  ∞Metcxmet 21337  ballcbl 21339  MetOpencmopn 21342  metUnifcmetu 21343   Cn ccn 23189  Compccmp 23351   Cnucucn 24239
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-er 8643  df-map 8775  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-sup 9355  df-inf 9356  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-n0 12438  df-z 12525  df-uz 12789  df-q 12899  df-rp 12943  df-xneg 13063  df-xadd 13064  df-xmul 13065  df-ico 13304  df-topgen 17406  df-psmet 21344  df-xmet 21345  df-bl 21347  df-mopn 21348  df-fbas 21349  df-fg 21350  df-metu 21351  df-top 22859  df-topon 22876  df-bases 22911  df-cn 23192  df-cnp 23193  df-cmp 23352  df-fil 23811  df-ust 24166  df-ucn 24240
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator