Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prdstotbnd Structured version   Visualization version   GIF version

Theorem prdstotbnd 37156
Description: The product metric over finite index set is totally bounded if all the factors are totally bounded. (Contributed by Mario Carneiro, 20-Sep-2015.)
Hypotheses
Ref Expression
prdsbnd.y 𝑌 = (𝑆Xs𝑅)
prdsbnd.b 𝐵 = (Base‘𝑌)
prdsbnd.v 𝑉 = (Base‘(𝑅𝑥))
prdsbnd.e 𝐸 = ((dist‘(𝑅𝑥)) ↾ (𝑉 × 𝑉))
prdsbnd.d 𝐷 = (dist‘𝑌)
prdsbnd.s (𝜑𝑆𝑊)
prdsbnd.i (𝜑𝐼 ∈ Fin)
prdsbnd.r (𝜑𝑅 Fn 𝐼)
prdstotbnd.m ((𝜑𝑥𝐼) → 𝐸 ∈ (TotBnd‘𝑉))
Assertion
Ref Expression
prdstotbnd (𝜑𝐷 ∈ (TotBnd‘𝐵))
Distinct variable groups:   𝑥,𝑅   𝑥,𝐵   𝜑,𝑥   𝑥,𝐼   𝑥,𝑆   𝑥,𝑌
Allowed substitution hints:   𝐷(𝑥)   𝐸(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem prdstotbnd
Dummy variables 𝑧 𝑟 𝑓 𝑔 𝑣 𝑦 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2724 . . . 4 (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))
2 eqid 2724 . . . 4 (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
3 prdsbnd.v . . . 4 𝑉 = (Base‘(𝑅𝑥))
4 prdsbnd.e . . . 4 𝐸 = ((dist‘(𝑅𝑥)) ↾ (𝑉 × 𝑉))
5 eqid 2724 . . . 4 (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
6 prdsbnd.s . . . 4 (𝜑𝑆𝑊)
7 prdsbnd.i . . . 4 (𝜑𝐼 ∈ Fin)
8 fvexd 6897 . . . 4 ((𝜑𝑥𝐼) → (𝑅𝑥) ∈ V)
9 prdstotbnd.m . . . . 5 ((𝜑𝑥𝐼) → 𝐸 ∈ (TotBnd‘𝑉))
10 totbndmet 37134 . . . . 5 (𝐸 ∈ (TotBnd‘𝑉) → 𝐸 ∈ (Met‘𝑉))
119, 10syl 17 . . . 4 ((𝜑𝑥𝐼) → 𝐸 ∈ (Met‘𝑉))
121, 2, 3, 4, 5, 6, 7, 8, 11prdsmet 24200 . . 3 (𝜑 → (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) ∈ (Met‘(Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))))
13 prdsbnd.d . . . 4 𝐷 = (dist‘𝑌)
14 prdsbnd.y . . . . . 6 𝑌 = (𝑆Xs𝑅)
15 prdsbnd.r . . . . . . . 8 (𝜑𝑅 Fn 𝐼)
16 dffn5 6941 . . . . . . . 8 (𝑅 Fn 𝐼𝑅 = (𝑥𝐼 ↦ (𝑅𝑥)))
1715, 16sylib 217 . . . . . . 7 (𝜑𝑅 = (𝑥𝐼 ↦ (𝑅𝑥)))
1817oveq2d 7418 . . . . . 6 (𝜑 → (𝑆Xs𝑅) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
1914, 18eqtrid 2776 . . . . 5 (𝜑𝑌 = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
2019fveq2d 6886 . . . 4 (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2113, 20eqtrid 2776 . . 3 (𝜑𝐷 = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
22 prdsbnd.b . . . . 5 𝐵 = (Base‘𝑌)
2319fveq2d 6886 . . . . 5 (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2422, 23eqtrid 2776 . . . 4 (𝜑𝐵 = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2524fveq2d 6886 . . 3 (𝜑 → (Met‘𝐵) = (Met‘(Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))))
2612, 21, 253eltr4d 2840 . 2 (𝜑𝐷 ∈ (Met‘𝐵))
277adantr 480 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → 𝐼 ∈ Fin)
28 istotbnd3 37133 . . . . . . . . . . 11 (𝐸 ∈ (TotBnd‘𝑉) ↔ (𝐸 ∈ (Met‘𝑉) ∧ ∀𝑟 ∈ ℝ+𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
2928simprbi 496 . . . . . . . . . 10 (𝐸 ∈ (TotBnd‘𝑉) → ∀𝑟 ∈ ℝ+𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)
309, 29syl 17 . . . . . . . . 9 ((𝜑𝑥𝐼) → ∀𝑟 ∈ ℝ+𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)
3130r19.21bi 3240 . . . . . . . 8 (((𝜑𝑥𝐼) ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)
32 df-rex 3063 . . . . . . . . 9 (∃𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 ↔ ∃𝑤(𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
33 rexv 3492 . . . . . . . . 9 (∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉) ↔ ∃𝑤(𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
3432, 33bitr4i 278 . . . . . . . 8 (∃𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 ↔ ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
3531, 34sylib 217 . . . . . . 7 (((𝜑𝑥𝐼) ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
3635an32s 649 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑥𝐼) → ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
3736ralrimiva 3138 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → ∀𝑥𝐼𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
38 eleq1 2813 . . . . . . 7 (𝑤 = (𝑓𝑥) → (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ↔ (𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin)))
39 iuneq1 5004 . . . . . . . 8 (𝑤 = (𝑓𝑥) → 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟))
4039eqeq1d 2726 . . . . . . 7 (𝑤 = (𝑓𝑥) → ( 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))
4138, 40anbi12d 630 . . . . . 6 (𝑤 = (𝑓𝑥) → ((𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉) ↔ ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉)))
4241ac6sfi 9284 . . . . 5 ((𝐼 ∈ Fin ∧ ∀𝑥𝐼𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)) → ∃𝑓(𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉)))
4327, 37, 42syl2anc 583 . . . 4 ((𝜑𝑟 ∈ ℝ+) → ∃𝑓(𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉)))
44 elfpw 9351 . . . . . . . . . . . 12 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ↔ ((𝑓𝑥) ⊆ 𝑉 ∧ (𝑓𝑥) ∈ Fin))
4544simplbi 497 . . . . . . . . . . 11 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) → (𝑓𝑥) ⊆ 𝑉)
4645adantr 480 . . . . . . . . . 10 (((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (𝑓𝑥) ⊆ 𝑉)
4746ralimi 3075 . . . . . . . . 9 (∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ∀𝑥𝐼 (𝑓𝑥) ⊆ 𝑉)
4847ad2antll 726 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑥𝐼 (𝑓𝑥) ⊆ 𝑉)
49 ss2ixp 8901 . . . . . . . 8 (∀𝑥𝐼 (𝑓𝑥) ⊆ 𝑉X𝑥𝐼 (𝑓𝑥) ⊆ X𝑥𝐼 𝑉)
5048, 49syl 17 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥𝐼 (𝑓𝑥) ⊆ X𝑥𝐼 𝑉)
51 fnfi 9178 . . . . . . . . . . 11 ((𝑅 Fn 𝐼𝐼 ∈ Fin) → 𝑅 ∈ Fin)
5215, 7, 51syl2anc 583 . . . . . . . . . 10 (𝜑𝑅 ∈ Fin)
5315fndmd 6645 . . . . . . . . . 10 (𝜑 → dom 𝑅 = 𝐼)
5414, 6, 52, 22, 53prdsbas 17404 . . . . . . . . 9 (𝜑𝐵 = X𝑥𝐼 (Base‘(𝑅𝑥)))
553rgenw 3057 . . . . . . . . . 10 𝑥𝐼 𝑉 = (Base‘(𝑅𝑥))
56 ixpeq2 8902 . . . . . . . . . 10 (∀𝑥𝐼 𝑉 = (Base‘(𝑅𝑥)) → X𝑥𝐼 𝑉 = X𝑥𝐼 (Base‘(𝑅𝑥)))
5755, 56ax-mp 5 . . . . . . . . 9 X𝑥𝐼 𝑉 = X𝑥𝐼 (Base‘(𝑅𝑥))
5854, 57eqtr4di 2782 . . . . . . . 8 (𝜑𝐵 = X𝑥𝐼 𝑉)
5958ad2antrr 723 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐵 = X𝑥𝐼 𝑉)
6050, 59sseqtrrd 4016 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥𝐼 (𝑓𝑥) ⊆ 𝐵)
6127adantr 480 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐼 ∈ Fin)
6244simprbi 496 . . . . . . . . . 10 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) → (𝑓𝑥) ∈ Fin)
6362adantr 480 . . . . . . . . 9 (((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (𝑓𝑥) ∈ Fin)
6463ralimi 3075 . . . . . . . 8 (∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ∀𝑥𝐼 (𝑓𝑥) ∈ Fin)
6564ad2antll 726 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑥𝐼 (𝑓𝑥) ∈ Fin)
66 ixpfi 9346 . . . . . . 7 ((𝐼 ∈ Fin ∧ ∀𝑥𝐼 (𝑓𝑥) ∈ Fin) → X𝑥𝐼 (𝑓𝑥) ∈ Fin)
6761, 65, 66syl2anc 583 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥𝐼 (𝑓𝑥) ∈ Fin)
68 elfpw 9351 . . . . . 6 (X𝑥𝐼 (𝑓𝑥) ∈ (𝒫 𝐵 ∩ Fin) ↔ (X𝑥𝐼 (𝑓𝑥) ⊆ 𝐵X𝑥𝐼 (𝑓𝑥) ∈ Fin))
6960, 67, 68sylanbrc 582 . . . . 5 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥𝐼 (𝑓𝑥) ∈ (𝒫 𝐵 ∩ Fin))
70 metxmet 24164 . . . . . . . . . . 11 (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵))
7126, 70syl 17 . . . . . . . . . 10 (𝜑𝐷 ∈ (∞Met‘𝐵))
72 rpxr 12981 . . . . . . . . . 10 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
73 blssm 24248 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑦𝐵𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
74733expa 1115 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑦𝐵) ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
7574an32s 649 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑟 ∈ ℝ*) ∧ 𝑦𝐵) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
7675ralrimiva 3138 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑟 ∈ ℝ*) → ∀𝑦𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
7771, 72, 76syl2an 595 . . . . . . . . 9 ((𝜑𝑟 ∈ ℝ+) → ∀𝑦𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
7877adantr 480 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑦𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
79 ssralv 4043 . . . . . . . 8 (X𝑥𝐼 (𝑓𝑥) ⊆ 𝐵 → (∀𝑦𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵 → ∀𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵))
8060, 78, 79sylc 65 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
81 iunss 5039 . . . . . . 7 ( 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵 ↔ ∀𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
8280, 81sylibr 233 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
8361adantr 480 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → 𝐼 ∈ Fin)
8459eleq2d 2811 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔𝐵𝑔X𝑥𝐼 𝑉))
85 vex 3470 . . . . . . . . . . . . . . . 16 𝑔 ∈ V
8685elixp 8895 . . . . . . . . . . . . . . 15 (𝑔X𝑥𝐼 𝑉 ↔ (𝑔 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉))
8786simprbi 496 . . . . . . . . . . . . . 14 (𝑔X𝑥𝐼 𝑉 → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
88 df-rex 3063 . . . . . . . . . . . . . . . . . . . 20 (∃𝑧 ∈ (𝑓𝑥)(𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧(𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
89 eliun 4992 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑥) ∈ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧 ∈ (𝑓𝑥)(𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))
90 rexv 3492 . . . . . . . . . . . . . . . . . . . 20 (∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ ∃𝑧(𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
9188, 89, 903bitr4i 303 . . . . . . . . . . . . . . . . . . 19 ((𝑔𝑥) ∈ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
92 eleq2 2814 . . . . . . . . . . . . . . . . . . 19 ( 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → ((𝑔𝑥) ∈ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) ↔ (𝑔𝑥) ∈ 𝑉))
9391, 92bitr3id 285 . . . . . . . . . . . . . . . . . 18 ( 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → (∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ (𝑔𝑥) ∈ 𝑉))
9493biimprd 247 . . . . . . . . . . . . . . . . 17 ( 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → ((𝑔𝑥) ∈ 𝑉 → ∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
9594adantl 481 . . . . . . . . . . . . . . . 16 (((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ((𝑔𝑥) ∈ 𝑉 → ∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
9695ral2imi 3077 . . . . . . . . . . . . . . 15 (∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉 → ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
9796ad2antll 726 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉 → ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
9887, 97syl5 34 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔X𝑥𝐼 𝑉 → ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
9984, 98sylbid 239 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔𝐵 → ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
10099imp 406 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
101 eleq1 2813 . . . . . . . . . . . . 13 (𝑧 = (𝑦𝑥) → (𝑧 ∈ (𝑓𝑥) ↔ (𝑦𝑥) ∈ (𝑓𝑥)))
102 oveq1 7409 . . . . . . . . . . . . . 14 (𝑧 = (𝑦𝑥) → (𝑧(ball‘𝐸)𝑟) = ((𝑦𝑥)(ball‘𝐸)𝑟))
103102eleq2d 2811 . . . . . . . . . . . . 13 (𝑧 = (𝑦𝑥) → ((𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟) ↔ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))
104101, 103anbi12d 630 . . . . . . . . . . . 12 (𝑧 = (𝑦𝑥) → ((𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))))
105104ac6sfi 9284 . . . . . . . . . . 11 ((𝐼 ∈ Fin ∧ ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))) → ∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))))
10683, 100, 105syl2anc 583 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → ∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))))
107 ffn 6708 . . . . . . . . . . . . . . . . 17 (𝑦:𝐼⟶V → 𝑦 Fn 𝐼)
108 simpl 482 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)) → (𝑦𝑥) ∈ (𝑓𝑥))
109108ralimi 3075 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)) → ∀𝑥𝐼 (𝑦𝑥) ∈ (𝑓𝑥))
110107, 109anim12i 612 . . . . . . . . . . . . . . . 16 ((𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → (𝑦 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑦𝑥) ∈ (𝑓𝑥)))
111 vex 3470 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
112111elixp 8895 . . . . . . . . . . . . . . . 16 (𝑦X𝑥𝐼 (𝑓𝑥) ↔ (𝑦 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑦𝑥) ∈ (𝑓𝑥)))
113110, 112sylibr 233 . . . . . . . . . . . . . . 15 ((𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → 𝑦X𝑥𝐼 (𝑓𝑥))
114113adantl 481 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑦X𝑥𝐼 (𝑓𝑥))
11584biimpa 476 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → 𝑔X𝑥𝐼 𝑉)
116 ixpfn 8894 . . . . . . . . . . . . . . . . . 18 (𝑔X𝑥𝐼 𝑉𝑔 Fn 𝐼)
117115, 116syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → 𝑔 Fn 𝐼)
118117adantr 480 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑔 Fn 𝐼)
119 simpr 484 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)) → (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))
120119ralimi 3075 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)) → ∀𝑥𝐼 (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))
121120ad2antll 726 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → ∀𝑥𝐼 (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))
12285elixp 8895 . . . . . . . . . . . . . . . 16 (𝑔X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))
123118, 121, 122sylanbrc 582 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑔X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟))
124 simp-4l 780 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝜑)
12550ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → X𝑥𝐼 (𝑓𝑥) ⊆ X𝑥𝐼 𝑉)
126125, 114sseldd 3976 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑦X𝑥𝐼 𝑉)
127124, 58syl 17 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝐵 = X𝑥𝐼 𝑉)
128126, 127eleqtrrd 2828 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑦𝐵)
129 simp-4r 781 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑟 ∈ ℝ+)
130 fveq2 6882 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑥 → (𝑅𝑦) = (𝑅𝑥))
131130cbvmptv 5252 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐼 ↦ (𝑅𝑦)) = (𝑥𝐼 ↦ (𝑅𝑥))
132131oveq2i 7413 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))
13319, 132eqtr4di 2782 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑌 = (𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))
134133fveq2d 6886 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
13513, 134eqtrid 2776 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 = (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
136135fveq2d 6886 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ball‘𝐷) = (ball‘(dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))))
137136oveqdr 7430 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘(dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))𝑟))
138 eqid 2724 . . . . . . . . . . . . . . . . . 18 (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))) = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))
139 eqid 2724 . . . . . . . . . . . . . . . . . 18 (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))) = (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))
1406adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝑆𝑊)
1417adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝐼 ∈ Fin)
142 fvexd 6897 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (𝑅𝑥) ∈ V)
143 metxmet 24164 . . . . . . . . . . . . . . . . . . . 20 (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉))
14411, 143syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
145144adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
146 simprl 768 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝑦𝐵)
147133fveq2d 6886 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
14822, 147eqtrid 2776 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
149148adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝐵 = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
150146, 149eleqtrd 2827 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝑦 ∈ (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
15172ad2antll 726 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ*)
152 rpgt0 12984 . . . . . . . . . . . . . . . . . . 19 (𝑟 ∈ ℝ+ → 0 < 𝑟)
153152ad2antll 726 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 0 < 𝑟)
154132, 138, 3, 4, 139, 140, 141, 142, 145, 150, 151, 153prdsbl 24324 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → (𝑦(ball‘(dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))𝑟) = X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟))
155137, 154eqtrd 2764 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → (𝑦(ball‘𝐷)𝑟) = X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟))
156124, 128, 129, 155syl12anc 834 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → (𝑦(ball‘𝐷)𝑟) = X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟))
157123, 156eleqtrrd 2828 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))
158114, 157jca 511 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → (𝑦X𝑥𝐼 (𝑓𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
159158ex 412 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → ((𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → (𝑦X𝑥𝐼 (𝑓𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))))
160159eximdv 1912 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → (∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → ∃𝑦(𝑦X𝑥𝐼 (𝑓𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))))
161 df-rex 3063 . . . . . . . . . . 11 (∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦(𝑦X𝑥𝐼 (𝑓𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
162160, 161imbitrrdi 251 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → (∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → ∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
163106, 162mpd 15 . . . . . . . . 9 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → ∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟))
164163ex 412 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔𝐵 → ∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
165 eliun 4992 . . . . . . . 8 (𝑔 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟))
166164, 165imbitrrdi 251 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔𝐵𝑔 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟)))
167166ssrdv 3981 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐵 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟))
16882, 167eqssd 3992 . . . . 5 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵)
169 iuneq1 5004 . . . . . . 7 (𝑣 = X𝑥𝐼 (𝑓𝑥) → 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟))
170169eqeq1d 2726 . . . . . 6 (𝑣 = X𝑥𝐼 (𝑓𝑥) → ( 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵))
171170rspcev 3604 . . . . 5 ((X𝑥𝐼 (𝑓𝑥) ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
17269, 168, 171syl2anc 583 . . . 4 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
17343, 172exlimddv 1930 . . 3 ((𝜑𝑟 ∈ ℝ+) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
174173ralrimiva 3138 . 2 (𝜑 → ∀𝑟 ∈ ℝ+𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
175 istotbnd3 37133 . 2 (𝐷 ∈ (TotBnd‘𝐵) ↔ (𝐷 ∈ (Met‘𝐵) ∧ ∀𝑟 ∈ ℝ+𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵))
17626, 174, 175sylanbrc 582 1 (𝜑𝐷 ∈ (TotBnd‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1533  wex 1773  wcel 2098  wral 3053  wrex 3062  Vcvv 3466  cin 3940  wss 3941  𝒫 cpw 4595   ciun 4988   class class class wbr 5139  cmpt 5222   × cxp 5665  cres 5669   Fn wfn 6529  wf 6530  cfv 6534  (class class class)co 7402  Xcixp 8888  Fincfn 8936  0cc0 11107  *cxr 11245   < clt 11246  +crp 12972  Basecbs 17145  distcds 17207  Xscprds 17392  ∞Metcxmet 21215  Metcmet 21216  ballcbl 21217  TotBndctotbnd 37128
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-tp 4626  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-1st 7969  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8700  df-map 8819  df-pm 8820  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-sup 9434  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252  df-sub 11444  df-neg 11445  df-div 11870  df-nn 12211  df-2 12273  df-3 12274  df-4 12275  df-5 12276  df-6 12277  df-7 12278  df-8 12279  df-9 12280  df-n0 12471  df-z 12557  df-dec 12676  df-uz 12821  df-rp 12973  df-xneg 13090  df-xadd 13091  df-xmul 13092  df-icc 13329  df-fz 13483  df-struct 17081  df-slot 17116  df-ndx 17128  df-base 17146  df-plusg 17211  df-mulr 17212  df-sca 17214  df-vsca 17215  df-ip 17216  df-tset 17217  df-ple 17218  df-ds 17220  df-hom 17222  df-cco 17223  df-prds 17394  df-psmet 21222  df-xmet 21223  df-met 21224  df-bl 21225  df-totbnd 37130
This theorem is referenced by:  prdsbnd2  37157
  Copyright terms: Public domain W3C validator