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 35575
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 2738 . . . 4 (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))
2 eqid 2738 . . . 4 (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
3 prdsbnd.v . . . 4 𝑉 = (Base‘(𝑅𝑥))
4 prdsbnd.e . . . 4 𝐸 = ((dist‘(𝑅𝑥)) ↾ (𝑉 × 𝑉))
5 eqid 2738 . . . 4 (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
6 prdsbnd.s . . . 4 (𝜑𝑆𝑊)
7 prdsbnd.i . . . 4 (𝜑𝐼 ∈ Fin)
8 fvexd 6689 . . . 4 ((𝜑𝑥𝐼) → (𝑅𝑥) ∈ V)
9 prdstotbnd.m . . . . 5 ((𝜑𝑥𝐼) → 𝐸 ∈ (TotBnd‘𝑉))
10 totbndmet 35553 . . . . 5 (𝐸 ∈ (TotBnd‘𝑉) → 𝐸 ∈ (Met‘𝑉))
119, 10syl 17 . . . 4 ((𝜑𝑥𝐼) → 𝐸 ∈ (Met‘𝑉))
121, 2, 3, 4, 5, 6, 7, 8, 11prdsmet 23123 . . 3 (𝜑 → (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) ∈ (Met‘(Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))))
13 prdsbnd.d . . . 4 𝐷 = (dist‘𝑌)
14 prdsbnd.y . . . . . 6 𝑌 = (𝑆Xs𝑅)
15 prdsbnd.r . . . . . . . 8 (𝜑𝑅 Fn 𝐼)
16 dffn5 6728 . . . . . . . 8 (𝑅 Fn 𝐼𝑅 = (𝑥𝐼 ↦ (𝑅𝑥)))
1715, 16sylib 221 . . . . . . 7 (𝜑𝑅 = (𝑥𝐼 ↦ (𝑅𝑥)))
1817oveq2d 7186 . . . . . 6 (𝜑 → (𝑆Xs𝑅) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
1914, 18syl5eq 2785 . . . . 5 (𝜑𝑌 = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
2019fveq2d 6678 . . . 4 (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2113, 20syl5eq 2785 . . 3 (𝜑𝐷 = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
22 prdsbnd.b . . . . 5 𝐵 = (Base‘𝑌)
2319fveq2d 6678 . . . . 5 (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2422, 23syl5eq 2785 . . . 4 (𝜑𝐵 = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2524fveq2d 6678 . . 3 (𝜑 → (Met‘𝐵) = (Met‘(Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))))
2612, 21, 253eltr4d 2848 . 2 (𝜑𝐷 ∈ (Met‘𝐵))
277adantr 484 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → 𝐼 ∈ Fin)
28 istotbnd3 35552 . . . . . . . . . . 11 (𝐸 ∈ (TotBnd‘𝑉) ↔ (𝐸 ∈ (Met‘𝑉) ∧ ∀𝑟 ∈ ℝ+𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
2928simprbi 500 . . . . . . . . . 10 (𝐸 ∈ (TotBnd‘𝑉) → ∀𝑟 ∈ ℝ+𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)
309, 29syl 17 . . . . . . . . 9 ((𝜑𝑥𝐼) → ∀𝑟 ∈ ℝ+𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)
3130r19.21bi 3121 . . . . . . . 8 (((𝜑𝑥𝐼) ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)
32 df-rex 3059 . . . . . . . . 9 (∃𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 ↔ ∃𝑤(𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
33 rexv 3423 . . . . . . . . 9 (∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉) ↔ ∃𝑤(𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
3432, 33bitr4i 281 . . . . . . . 8 (∃𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 ↔ ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
3531, 34sylib 221 . . . . . . 7 (((𝜑𝑥𝐼) ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
3635an32s 652 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑥𝐼) → ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
3736ralrimiva 3096 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → ∀𝑥𝐼𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
38 eleq1 2820 . . . . . . 7 (𝑤 = (𝑓𝑥) → (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ↔ (𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin)))
39 iuneq1 4897 . . . . . . . 8 (𝑤 = (𝑓𝑥) → 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟))
4039eqeq1d 2740 . . . . . . 7 (𝑤 = (𝑓𝑥) → ( 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))
4138, 40anbi12d 634 . . . . . 6 (𝑤 = (𝑓𝑥) → ((𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉) ↔ ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉)))
4241ac6sfi 8836 . . . . 5 ((𝐼 ∈ Fin ∧ ∀𝑥𝐼𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)) → ∃𝑓(𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉)))
4327, 37, 42syl2anc 587 . . . 4 ((𝜑𝑟 ∈ ℝ+) → ∃𝑓(𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉)))
44 elfpw 8899 . . . . . . . . . . . 12 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ↔ ((𝑓𝑥) ⊆ 𝑉 ∧ (𝑓𝑥) ∈ Fin))
4544simplbi 501 . . . . . . . . . . 11 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) → (𝑓𝑥) ⊆ 𝑉)
4645adantr 484 . . . . . . . . . 10 (((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (𝑓𝑥) ⊆ 𝑉)
4746ralimi 3075 . . . . . . . . 9 (∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ∀𝑥𝐼 (𝑓𝑥) ⊆ 𝑉)
4847ad2antll 729 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑥𝐼 (𝑓𝑥) ⊆ 𝑉)
49 ss2ixp 8520 . . . . . . . 8 (∀𝑥𝐼 (𝑓𝑥) ⊆ 𝑉X𝑥𝐼 (𝑓𝑥) ⊆ X𝑥𝐼 𝑉)
5048, 49syl 17 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥𝐼 (𝑓𝑥) ⊆ X𝑥𝐼 𝑉)
51 fnfi 8778 . . . . . . . . . . 11 ((𝑅 Fn 𝐼𝐼 ∈ Fin) → 𝑅 ∈ Fin)
5215, 7, 51syl2anc 587 . . . . . . . . . 10 (𝜑𝑅 ∈ Fin)
5315fndmd 6442 . . . . . . . . . 10 (𝜑 → dom 𝑅 = 𝐼)
5414, 6, 52, 22, 53prdsbas 16833 . . . . . . . . 9 (𝜑𝐵 = X𝑥𝐼 (Base‘(𝑅𝑥)))
553rgenw 3065 . . . . . . . . . 10 𝑥𝐼 𝑉 = (Base‘(𝑅𝑥))
56 ixpeq2 8521 . . . . . . . . . 10 (∀𝑥𝐼 𝑉 = (Base‘(𝑅𝑥)) → X𝑥𝐼 𝑉 = X𝑥𝐼 (Base‘(𝑅𝑥)))
5755, 56ax-mp 5 . . . . . . . . 9 X𝑥𝐼 𝑉 = X𝑥𝐼 (Base‘(𝑅𝑥))
5854, 57eqtr4di 2791 . . . . . . . 8 (𝜑𝐵 = X𝑥𝐼 𝑉)
5958ad2antrr 726 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐵 = X𝑥𝐼 𝑉)
6050, 59sseqtrrd 3918 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥𝐼 (𝑓𝑥) ⊆ 𝐵)
6127adantr 484 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐼 ∈ Fin)
6244simprbi 500 . . . . . . . . . 10 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) → (𝑓𝑥) ∈ Fin)
6362adantr 484 . . . . . . . . 9 (((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (𝑓𝑥) ∈ Fin)
6463ralimi 3075 . . . . . . . 8 (∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ∀𝑥𝐼 (𝑓𝑥) ∈ Fin)
6564ad2antll 729 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑥𝐼 (𝑓𝑥) ∈ Fin)
66 ixpfi 8894 . . . . . . 7 ((𝐼 ∈ Fin ∧ ∀𝑥𝐼 (𝑓𝑥) ∈ Fin) → X𝑥𝐼 (𝑓𝑥) ∈ Fin)
6761, 65, 66syl2anc 587 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥𝐼 (𝑓𝑥) ∈ Fin)
68 elfpw 8899 . . . . . 6 (X𝑥𝐼 (𝑓𝑥) ∈ (𝒫 𝐵 ∩ Fin) ↔ (X𝑥𝐼 (𝑓𝑥) ⊆ 𝐵X𝑥𝐼 (𝑓𝑥) ∈ Fin))
6960, 67, 68sylanbrc 586 . . . . 5 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥𝐼 (𝑓𝑥) ∈ (𝒫 𝐵 ∩ Fin))
70 metxmet 23087 . . . . . . . . . . 11 (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵))
7126, 70syl 17 . . . . . . . . . 10 (𝜑𝐷 ∈ (∞Met‘𝐵))
72 rpxr 12481 . . . . . . . . . 10 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
73 blssm 23171 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑦𝐵𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
74733expa 1119 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑦𝐵) ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
7574an32s 652 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑟 ∈ ℝ*) ∧ 𝑦𝐵) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
7675ralrimiva 3096 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑟 ∈ ℝ*) → ∀𝑦𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
7771, 72, 76syl2an 599 . . . . . . . . 9 ((𝜑𝑟 ∈ ℝ+) → ∀𝑦𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
7877adantr 484 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑦𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
79 ssralv 3943 . . . . . . . 8 (X𝑥𝐼 (𝑓𝑥) ⊆ 𝐵 → (∀𝑦𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵 → ∀𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵))
8060, 78, 79sylc 65 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
81 iunss 4931 . . . . . . 7 ( 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵 ↔ ∀𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
8280, 81sylibr 237 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
8361adantr 484 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → 𝐼 ∈ Fin)
8459eleq2d 2818 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔𝐵𝑔X𝑥𝐼 𝑉))
85 vex 3402 . . . . . . . . . . . . . . . 16 𝑔 ∈ V
8685elixp 8514 . . . . . . . . . . . . . . 15 (𝑔X𝑥𝐼 𝑉 ↔ (𝑔 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉))
8786simprbi 500 . . . . . . . . . . . . . 14 (𝑔X𝑥𝐼 𝑉 → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
88 df-rex 3059 . . . . . . . . . . . . . . . . . . . 20 (∃𝑧 ∈ (𝑓𝑥)(𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧(𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
89 eliun 4885 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑥) ∈ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧 ∈ (𝑓𝑥)(𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))
90 rexv 3423 . . . . . . . . . . . . . . . . . . . 20 (∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ ∃𝑧(𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
9188, 89, 903bitr4i 306 . . . . . . . . . . . . . . . . . . 19 ((𝑔𝑥) ∈ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
92 eleq2 2821 . . . . . . . . . . . . . . . . . . 19 ( 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → ((𝑔𝑥) ∈ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) ↔ (𝑔𝑥) ∈ 𝑉))
9391, 92bitr3id 288 . . . . . . . . . . . . . . . . . 18 ( 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → (∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ (𝑔𝑥) ∈ 𝑉))
9493biimprd 251 . . . . . . . . . . . . . . . . 17 ( 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → ((𝑔𝑥) ∈ 𝑉 → ∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
9594adantl 485 . . . . . . . . . . . . . . . 16 (((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ((𝑔𝑥) ∈ 𝑉 → ∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
9695ral2imi 3071 . . . . . . . . . . . . . . 15 (∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉 → ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
9796ad2antll 729 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉 → ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
9887, 97syl5 34 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔X𝑥𝐼 𝑉 → ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
9984, 98sylbid 243 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔𝐵 → ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
10099imp 410 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
101 eleq1 2820 . . . . . . . . . . . . 13 (𝑧 = (𝑦𝑥) → (𝑧 ∈ (𝑓𝑥) ↔ (𝑦𝑥) ∈ (𝑓𝑥)))
102 oveq1 7177 . . . . . . . . . . . . . 14 (𝑧 = (𝑦𝑥) → (𝑧(ball‘𝐸)𝑟) = ((𝑦𝑥)(ball‘𝐸)𝑟))
103102eleq2d 2818 . . . . . . . . . . . . 13 (𝑧 = (𝑦𝑥) → ((𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟) ↔ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))
104101, 103anbi12d 634 . . . . . . . . . . . 12 (𝑧 = (𝑦𝑥) → ((𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))))
105104ac6sfi 8836 . . . . . . . . . . 11 ((𝐼 ∈ Fin ∧ ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))) → ∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))))
10683, 100, 105syl2anc 587 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → ∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))))
107 ffn 6504 . . . . . . . . . . . . . . . . 17 (𝑦:𝐼⟶V → 𝑦 Fn 𝐼)
108 simpl 486 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)) → (𝑦𝑥) ∈ (𝑓𝑥))
109108ralimi 3075 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)) → ∀𝑥𝐼 (𝑦𝑥) ∈ (𝑓𝑥))
110107, 109anim12i 616 . . . . . . . . . . . . . . . 16 ((𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → (𝑦 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑦𝑥) ∈ (𝑓𝑥)))
111 vex 3402 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
112111elixp 8514 . . . . . . . . . . . . . . . 16 (𝑦X𝑥𝐼 (𝑓𝑥) ↔ (𝑦 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑦𝑥) ∈ (𝑓𝑥)))
113110, 112sylibr 237 . . . . . . . . . . . . . . 15 ((𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → 𝑦X𝑥𝐼 (𝑓𝑥))
114113adantl 485 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑦X𝑥𝐼 (𝑓𝑥))
11584biimpa 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → 𝑔X𝑥𝐼 𝑉)
116 ixpfn 8513 . . . . . . . . . . . . . . . . . 18 (𝑔X𝑥𝐼 𝑉𝑔 Fn 𝐼)
117115, 116syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → 𝑔 Fn 𝐼)
118117adantr 484 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑔 Fn 𝐼)
119 simpr 488 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)) → (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))
120119ralimi 3075 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)) → ∀𝑥𝐼 (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))
121120ad2antll 729 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → ∀𝑥𝐼 (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))
12285elixp 8514 . . . . . . . . . . . . . . . 16 (𝑔X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))
123118, 121, 122sylanbrc 586 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑔X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟))
124 simp-4l 783 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝜑)
12550ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → X𝑥𝐼 (𝑓𝑥) ⊆ X𝑥𝐼 𝑉)
126125, 114sseldd 3878 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑦X𝑥𝐼 𝑉)
127124, 58syl 17 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝐵 = X𝑥𝐼 𝑉)
128126, 127eleqtrrd 2836 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑦𝐵)
129 simp-4r 784 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑟 ∈ ℝ+)
130 fveq2 6674 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑥 → (𝑅𝑦) = (𝑅𝑥))
131130cbvmptv 5133 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐼 ↦ (𝑅𝑦)) = (𝑥𝐼 ↦ (𝑅𝑥))
132131oveq2i 7181 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))
13319, 132eqtr4di 2791 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑌 = (𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))
134133fveq2d 6678 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
13513, 134syl5eq 2785 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 = (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
136135fveq2d 6678 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ball‘𝐷) = (ball‘(dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))))
137136oveqdr 7198 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘(dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))𝑟))
138 eqid 2738 . . . . . . . . . . . . . . . . . 18 (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))) = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))
139 eqid 2738 . . . . . . . . . . . . . . . . . 18 (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))) = (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))
1406adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝑆𝑊)
1417adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝐼 ∈ Fin)
142 fvexd 6689 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (𝑅𝑥) ∈ V)
143 metxmet 23087 . . . . . . . . . . . . . . . . . . . 20 (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉))
14411, 143syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
145144adantlr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
146 simprl 771 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝑦𝐵)
147133fveq2d 6678 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
14822, 147syl5eq 2785 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
149148adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝐵 = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
150146, 149eleqtrd 2835 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝑦 ∈ (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
15172ad2antll 729 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ*)
152 rpgt0 12484 . . . . . . . . . . . . . . . . . . 19 (𝑟 ∈ ℝ+ → 0 < 𝑟)
153152ad2antll 729 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 0 < 𝑟)
154132, 138, 3, 4, 139, 140, 141, 142, 145, 150, 151, 153prdsbl 23244 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → (𝑦(ball‘(dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))𝑟) = X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟))
155137, 154eqtrd 2773 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → (𝑦(ball‘𝐷)𝑟) = X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟))
156124, 128, 129, 155syl12anc 836 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → (𝑦(ball‘𝐷)𝑟) = X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟))
157123, 156eleqtrrd 2836 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))
158114, 157jca 515 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → (𝑦X𝑥𝐼 (𝑓𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
159158ex 416 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → ((𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → (𝑦X𝑥𝐼 (𝑓𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))))
160159eximdv 1924 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → (∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → ∃𝑦(𝑦X𝑥𝐼 (𝑓𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))))
161 df-rex 3059 . . . . . . . . . . 11 (∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦(𝑦X𝑥𝐼 (𝑓𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
162160, 161syl6ibr 255 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → (∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → ∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
163106, 162mpd 15 . . . . . . . . 9 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → ∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟))
164163ex 416 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔𝐵 → ∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
165 eliun 4885 . . . . . . . 8 (𝑔 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟))
166164, 165syl6ibr 255 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔𝐵𝑔 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟)))
167166ssrdv 3883 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐵 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟))
16882, 167eqssd 3894 . . . . 5 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵)
169 iuneq1 4897 . . . . . . 7 (𝑣 = X𝑥𝐼 (𝑓𝑥) → 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟))
170169eqeq1d 2740 . . . . . 6 (𝑣 = X𝑥𝐼 (𝑓𝑥) → ( 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵))
171170rspcev 3526 . . . . 5 ((X𝑥𝐼 (𝑓𝑥) ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
17269, 168, 171syl2anc 587 . . . 4 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
17343, 172exlimddv 1942 . . 3 ((𝜑𝑟 ∈ ℝ+) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
174173ralrimiva 3096 . 2 (𝜑 → ∀𝑟 ∈ ℝ+𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
175 istotbnd3 35552 . 2 (𝐷 ∈ (TotBnd‘𝐵) ↔ (𝐷 ∈ (Met‘𝐵) ∧ ∀𝑟 ∈ ℝ+𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵))
17626, 174, 175sylanbrc 586 1 (𝜑𝐷 ∈ (TotBnd‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1542  wex 1786  wcel 2114  wral 3053  wrex 3054  Vcvv 3398  cin 3842  wss 3843  𝒫 cpw 4488   ciun 4881   class class class wbr 5030  cmpt 5110   × cxp 5523  cres 5527   Fn wfn 6334  wf 6335  cfv 6339  (class class class)co 7170  Xcixp 8507  Fincfn 8555  0cc0 10615  *cxr 10752   < clt 10753  +crp 12472  Basecbs 16586  distcds 16677  Xscprds 16822  ∞Metcxmet 20202  Metcmet 20203  ballcbl 20204  TotBndctotbnd 35547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-cnex 10671  ax-resscn 10672  ax-1cn 10673  ax-icn 10674  ax-addcl 10675  ax-addrcl 10676  ax-mulcl 10677  ax-mulrcl 10678  ax-mulcom 10679  ax-addass 10680  ax-mulass 10681  ax-distr 10682  ax-i2m1 10683  ax-1ne0 10684  ax-1rid 10685  ax-rnegex 10686  ax-rrecex 10687  ax-cnre 10688  ax-pre-lttri 10689  ax-pre-lttrn 10690  ax-pre-ltadd 10691  ax-pre-mulgt0 10692  ax-pre-sup 10693
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-om 7600  df-1st 7714  df-2nd 7715  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-1o 8131  df-er 8320  df-map 8439  df-pm 8440  df-ixp 8508  df-en 8556  df-dom 8557  df-sdom 8558  df-fin 8559  df-sup 8979  df-pnf 10755  df-mnf 10756  df-xr 10757  df-ltxr 10758  df-le 10759  df-sub 10950  df-neg 10951  df-div 11376  df-nn 11717  df-2 11779  df-3 11780  df-4 11781  df-5 11782  df-6 11783  df-7 11784  df-8 11785  df-9 11786  df-n0 11977  df-z 12063  df-dec 12180  df-uz 12325  df-rp 12473  df-xneg 12590  df-xadd 12591  df-xmul 12592  df-icc 12828  df-fz 12982  df-struct 16588  df-ndx 16589  df-slot 16590  df-base 16592  df-plusg 16681  df-mulr 16682  df-sca 16684  df-vsca 16685  df-ip 16686  df-tset 16687  df-ple 16688  df-ds 16690  df-hom 16692  df-cco 16693  df-prds 16824  df-psmet 20209  df-xmet 20210  df-met 20211  df-bl 20212  df-totbnd 35549
This theorem is referenced by:  prdsbnd2  35576
  Copyright terms: Public domain W3C validator