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 35961
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 2739 . . . 4 (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))
2 eqid 2739 . . . 4 (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
3 prdsbnd.v . . . 4 𝑉 = (Base‘(𝑅𝑥))
4 prdsbnd.e . . . 4 𝐸 = ((dist‘(𝑅𝑥)) ↾ (𝑉 × 𝑉))
5 eqid 2739 . . . 4 (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
6 prdsbnd.s . . . 4 (𝜑𝑆𝑊)
7 prdsbnd.i . . . 4 (𝜑𝐼 ∈ Fin)
8 fvexd 6798 . . . 4 ((𝜑𝑥𝐼) → (𝑅𝑥) ∈ V)
9 prdstotbnd.m . . . . 5 ((𝜑𝑥𝐼) → 𝐸 ∈ (TotBnd‘𝑉))
10 totbndmet 35939 . . . . 5 (𝐸 ∈ (TotBnd‘𝑉) → 𝐸 ∈ (Met‘𝑉))
119, 10syl 17 . . . 4 ((𝜑𝑥𝐼) → 𝐸 ∈ (Met‘𝑉))
121, 2, 3, 4, 5, 6, 7, 8, 11prdsmet 23532 . . 3 (𝜑 → (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))) ∈ (Met‘(Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))))
13 prdsbnd.d . . . 4 𝐷 = (dist‘𝑌)
14 prdsbnd.y . . . . . 6 𝑌 = (𝑆Xs𝑅)
15 prdsbnd.r . . . . . . . 8 (𝜑𝑅 Fn 𝐼)
16 dffn5 6837 . . . . . . . 8 (𝑅 Fn 𝐼𝑅 = (𝑥𝐼 ↦ (𝑅𝑥)))
1715, 16sylib 217 . . . . . . 7 (𝜑𝑅 = (𝑥𝐼 ↦ (𝑅𝑥)))
1817oveq2d 7300 . . . . . 6 (𝜑 → (𝑆Xs𝑅) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
1914, 18eqtrid 2791 . . . . 5 (𝜑𝑌 = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))
2019fveq2d 6787 . . . 4 (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2113, 20eqtrid 2791 . . 3 (𝜑𝐷 = (dist‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
22 prdsbnd.b . . . . 5 𝐵 = (Base‘𝑌)
2319fveq2d 6787 . . . . 5 (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2422, 23eqtrid 2791 . . . 4 (𝜑𝐵 = (Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))))
2524fveq2d 6787 . . 3 (𝜑 → (Met‘𝐵) = (Met‘(Base‘(𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥))))))
2612, 21, 253eltr4d 2855 . 2 (𝜑𝐷 ∈ (Met‘𝐵))
277adantr 481 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → 𝐼 ∈ Fin)
28 istotbnd3 35938 . . . . . . . . . . 11 (𝐸 ∈ (TotBnd‘𝑉) ↔ (𝐸 ∈ (Met‘𝑉) ∧ ∀𝑟 ∈ ℝ+𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
2928simprbi 497 . . . . . . . . . 10 (𝐸 ∈ (TotBnd‘𝑉) → ∀𝑟 ∈ ℝ+𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)
309, 29syl 17 . . . . . . . . 9 ((𝜑𝑥𝐼) → ∀𝑟 ∈ ℝ+𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)
3130r19.21bi 3135 . . . . . . . 8 (((𝜑𝑥𝐼) ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)
32 df-rex 3071 . . . . . . . . 9 (∃𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 ↔ ∃𝑤(𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
33 rexv 3458 . . . . . . . . 9 (∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉) ↔ ∃𝑤(𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
3432, 33bitr4i 277 . . . . . . . 8 (∃𝑤 ∈ (𝒫 𝑉 ∩ Fin) 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 ↔ ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
3531, 34sylib 217 . . . . . . 7 (((𝜑𝑥𝐼) ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
3635an32s 649 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑥𝐼) → ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
3736ralrimiva 3104 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → ∀𝑥𝐼𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
38 eleq1 2827 . . . . . . 7 (𝑤 = (𝑓𝑥) → (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ↔ (𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin)))
39 iuneq1 4941 . . . . . . . 8 (𝑤 = (𝑓𝑥) → 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟))
4039eqeq1d 2741 . . . . . . 7 (𝑤 = (𝑓𝑥) → ( 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))
4138, 40anbi12d 631 . . . . . 6 (𝑤 = (𝑓𝑥) → ((𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉) ↔ ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉)))
4241ac6sfi 9067 . . . . 5 ((𝐼 ∈ Fin ∧ ∀𝑥𝐼𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)) → ∃𝑓(𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉)))
4327, 37, 42syl2anc 584 . . . 4 ((𝜑𝑟 ∈ ℝ+) → ∃𝑓(𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉)))
44 elfpw 9130 . . . . . . . . . . . 12 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ↔ ((𝑓𝑥) ⊆ 𝑉 ∧ (𝑓𝑥) ∈ Fin))
4544simplbi 498 . . . . . . . . . . 11 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) → (𝑓𝑥) ⊆ 𝑉)
4645adantr 481 . . . . . . . . . 10 (((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (𝑓𝑥) ⊆ 𝑉)
4746ralimi 3088 . . . . . . . . 9 (∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ∀𝑥𝐼 (𝑓𝑥) ⊆ 𝑉)
4847ad2antll 726 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑥𝐼 (𝑓𝑥) ⊆ 𝑉)
49 ss2ixp 8707 . . . . . . . 8 (∀𝑥𝐼 (𝑓𝑥) ⊆ 𝑉X𝑥𝐼 (𝑓𝑥) ⊆ X𝑥𝐼 𝑉)
5048, 49syl 17 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥𝐼 (𝑓𝑥) ⊆ X𝑥𝐼 𝑉)
51 fnfi 8973 . . . . . . . . . . 11 ((𝑅 Fn 𝐼𝐼 ∈ Fin) → 𝑅 ∈ Fin)
5215, 7, 51syl2anc 584 . . . . . . . . . 10 (𝜑𝑅 ∈ Fin)
5315fndmd 6547 . . . . . . . . . 10 (𝜑 → dom 𝑅 = 𝐼)
5414, 6, 52, 22, 53prdsbas 17177 . . . . . . . . 9 (𝜑𝐵 = X𝑥𝐼 (Base‘(𝑅𝑥)))
553rgenw 3077 . . . . . . . . . 10 𝑥𝐼 𝑉 = (Base‘(𝑅𝑥))
56 ixpeq2 8708 . . . . . . . . . 10 (∀𝑥𝐼 𝑉 = (Base‘(𝑅𝑥)) → X𝑥𝐼 𝑉 = X𝑥𝐼 (Base‘(𝑅𝑥)))
5755, 56ax-mp 5 . . . . . . . . 9 X𝑥𝐼 𝑉 = X𝑥𝐼 (Base‘(𝑅𝑥))
5854, 57eqtr4di 2797 . . . . . . . 8 (𝜑𝐵 = X𝑥𝐼 𝑉)
5958ad2antrr 723 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐵 = X𝑥𝐼 𝑉)
6050, 59sseqtrrd 3963 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥𝐼 (𝑓𝑥) ⊆ 𝐵)
6127adantr 481 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐼 ∈ Fin)
6244simprbi 497 . . . . . . . . . 10 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) → (𝑓𝑥) ∈ Fin)
6362adantr 481 . . . . . . . . 9 (((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (𝑓𝑥) ∈ Fin)
6463ralimi 3088 . . . . . . . 8 (∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ∀𝑥𝐼 (𝑓𝑥) ∈ Fin)
6564ad2antll 726 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑥𝐼 (𝑓𝑥) ∈ Fin)
66 ixpfi 9125 . . . . . . 7 ((𝐼 ∈ Fin ∧ ∀𝑥𝐼 (𝑓𝑥) ∈ Fin) → X𝑥𝐼 (𝑓𝑥) ∈ Fin)
6761, 65, 66syl2anc 584 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥𝐼 (𝑓𝑥) ∈ Fin)
68 elfpw 9130 . . . . . 6 (X𝑥𝐼 (𝑓𝑥) ∈ (𝒫 𝐵 ∩ Fin) ↔ (X𝑥𝐼 (𝑓𝑥) ⊆ 𝐵X𝑥𝐼 (𝑓𝑥) ∈ Fin))
6960, 67, 68sylanbrc 583 . . . . 5 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥𝐼 (𝑓𝑥) ∈ (𝒫 𝐵 ∩ Fin))
70 metxmet 23496 . . . . . . . . . . 11 (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵))
7126, 70syl 17 . . . . . . . . . 10 (𝜑𝐷 ∈ (∞Met‘𝐵))
72 rpxr 12748 . . . . . . . . . 10 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
73 blssm 23580 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑦𝐵𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
74733expa 1117 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑦𝐵) ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
7574an32s 649 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑟 ∈ ℝ*) ∧ 𝑦𝐵) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
7675ralrimiva 3104 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑟 ∈ ℝ*) → ∀𝑦𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
7771, 72, 76syl2an 596 . . . . . . . . 9 ((𝜑𝑟 ∈ ℝ+) → ∀𝑦𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
7877adantr 481 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑦𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
79 ssralv 3988 . . . . . . . 8 (X𝑥𝐼 (𝑓𝑥) ⊆ 𝐵 → (∀𝑦𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵 → ∀𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵))
8060, 78, 79sylc 65 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
81 iunss 4976 . . . . . . 7 ( 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵 ↔ ∀𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
8280, 81sylibr 233 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
8361adantr 481 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → 𝐼 ∈ Fin)
8459eleq2d 2825 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔𝐵𝑔X𝑥𝐼 𝑉))
85 vex 3437 . . . . . . . . . . . . . . . 16 𝑔 ∈ V
8685elixp 8701 . . . . . . . . . . . . . . 15 (𝑔X𝑥𝐼 𝑉 ↔ (𝑔 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉))
8786simprbi 497 . . . . . . . . . . . . . 14 (𝑔X𝑥𝐼 𝑉 → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
88 df-rex 3071 . . . . . . . . . . . . . . . . . . . 20 (∃𝑧 ∈ (𝑓𝑥)(𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧(𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
89 eliun 4929 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑥) ∈ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧 ∈ (𝑓𝑥)(𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))
90 rexv 3458 . . . . . . . . . . . . . . . . . . . 20 (∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ ∃𝑧(𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
9188, 89, 903bitr4i 303 . . . . . . . . . . . . . . . . . . 19 ((𝑔𝑥) ∈ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
92 eleq2 2828 . . . . . . . . . . . . . . . . . . 19 ( 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → ((𝑔𝑥) ∈ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) ↔ (𝑔𝑥) ∈ 𝑉))
9391, 92bitr3id 285 . . . . . . . . . . . . . . . . . 18 ( 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → (∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ (𝑔𝑥) ∈ 𝑉))
9493biimprd 247 . . . . . . . . . . . . . . . . 17 ( 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → ((𝑔𝑥) ∈ 𝑉 → ∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
9594adantl 482 . . . . . . . . . . . . . . . 16 (((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ((𝑔𝑥) ∈ 𝑉 → ∃𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
9695ral2imi 3083 . . . . . . . . . . . . . . 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 407 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
101 eleq1 2827 . . . . . . . . . . . . 13 (𝑧 = (𝑦𝑥) → (𝑧 ∈ (𝑓𝑥) ↔ (𝑦𝑥) ∈ (𝑓𝑥)))
102 oveq1 7291 . . . . . . . . . . . . . 14 (𝑧 = (𝑦𝑥) → (𝑧(ball‘𝐸)𝑟) = ((𝑦𝑥)(ball‘𝐸)𝑟))
103102eleq2d 2825 . . . . . . . . . . . . 13 (𝑧 = (𝑦𝑥) → ((𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟) ↔ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))
104101, 103anbi12d 631 . . . . . . . . . . . 12 (𝑧 = (𝑦𝑥) → ((𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))))
105104ac6sfi 9067 . . . . . . . . . . 11 ((𝐼 ∈ Fin ∧ ∀𝑥𝐼𝑧 ∈ V (𝑧 ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ (𝑧(ball‘𝐸)𝑟))) → ∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))))
10683, 100, 105syl2anc 584 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → ∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))))
107 ffn 6609 . . . . . . . . . . . . . . . . 17 (𝑦:𝐼⟶V → 𝑦 Fn 𝐼)
108 simpl 483 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)) → (𝑦𝑥) ∈ (𝑓𝑥))
109108ralimi 3088 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)) → ∀𝑥𝐼 (𝑦𝑥) ∈ (𝑓𝑥))
110107, 109anim12i 613 . . . . . . . . . . . . . . . 16 ((𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → (𝑦 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑦𝑥) ∈ (𝑓𝑥)))
111 vex 3437 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
112111elixp 8701 . . . . . . . . . . . . . . . 16 (𝑦X𝑥𝐼 (𝑓𝑥) ↔ (𝑦 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑦𝑥) ∈ (𝑓𝑥)))
113110, 112sylibr 233 . . . . . . . . . . . . . . 15 ((𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → 𝑦X𝑥𝐼 (𝑓𝑥))
114113adantl 482 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑦X𝑥𝐼 (𝑓𝑥))
11584biimpa 477 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → 𝑔X𝑥𝐼 𝑉)
116 ixpfn 8700 . . . . . . . . . . . . . . . . . 18 (𝑔X𝑥𝐼 𝑉𝑔 Fn 𝐼)
117115, 116syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → 𝑔 Fn 𝐼)
118117adantr 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑔 Fn 𝐼)
119 simpr 485 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)) → (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))
120119ralimi 3088 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)) → ∀𝑥𝐼 (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))
121120ad2antll 726 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → ∀𝑥𝐼 (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))
12285elixp 8701 . . . . . . . . . . . . . . . 16 (𝑔X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))
123118, 121, 122sylanbrc 583 . . . . . . . . . . . . . . 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 3923 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑦X𝑥𝐼 𝑉)
127124, 58syl 17 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝐵 = X𝑥𝐼 𝑉)
128126, 127eleqtrrd 2843 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑦𝐵)
129 simp-4r 781 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑟 ∈ ℝ+)
130 fveq2 6783 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑥 → (𝑅𝑦) = (𝑅𝑥))
131130cbvmptv 5188 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐼 ↦ (𝑅𝑦)) = (𝑥𝐼 ↦ (𝑅𝑥))
132131oveq2i 7295 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))) = (𝑆Xs(𝑥𝐼 ↦ (𝑅𝑥)))
13319, 132eqtr4di 2797 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑌 = (𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))
134133fveq2d 6787 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
13513, 134eqtrid 2791 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 = (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
136135fveq2d 6787 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ball‘𝐷) = (ball‘(dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))))
137136oveqdr 7312 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘(dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))𝑟))
138 eqid 2739 . . . . . . . . . . . . . . . . . 18 (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))) = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))
139 eqid 2739 . . . . . . . . . . . . . . . . . 18 (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))) = (dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦))))
1406adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝑆𝑊)
1417adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝐼 ∈ Fin)
142 fvexd 6798 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → (𝑅𝑥) ∈ V)
143 metxmet 23496 . . . . . . . . . . . . . . . . . . . 20 (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉))
14411, 143syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
145144adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
146 simprl 768 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝑦𝐵)
147133fveq2d 6787 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
14822, 147eqtrid 2791 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
149148adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝐵 = (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
150146, 149eleqtrd 2842 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝑦 ∈ (Base‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))
15172ad2antll 726 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ*)
152 rpgt0 12751 . . . . . . . . . . . . . . . . . . 19 (𝑟 ∈ ℝ+ → 0 < 𝑟)
153152ad2antll 726 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → 0 < 𝑟)
154132, 138, 3, 4, 139, 140, 141, 142, 145, 150, 151, 153prdsbl 23656 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → (𝑦(ball‘(dist‘(𝑆Xs(𝑦𝐼 ↦ (𝑅𝑦)))))𝑟) = X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟))
155137, 154eqtrd 2779 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑦𝐵𝑟 ∈ ℝ+)) → (𝑦(ball‘𝐷)𝑟) = X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟))
156124, 128, 129, 155syl12anc 834 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → (𝑦(ball‘𝐷)𝑟) = X𝑥𝐼 ((𝑦𝑥)(ball‘𝐸)𝑟))
157123, 156eleqtrrd 2843 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))
158114, 157jca 512 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟)))) → (𝑦X𝑥𝐼 (𝑓𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
159158ex 413 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → ((𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → (𝑦X𝑥𝐼 (𝑓𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))))
160159eximdv 1921 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → (∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → ∃𝑦(𝑦X𝑥𝐼 (𝑓𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))))
161 df-rex 3071 . . . . . . . . . . 11 (∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦(𝑦X𝑥𝐼 (𝑓𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
162160, 161syl6ibr 251 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → (∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑦𝑥) ∈ (𝑓𝑥) ∧ (𝑔𝑥) ∈ ((𝑦𝑥)(ball‘𝐸)𝑟))) → ∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
163106, 162mpd 15 . . . . . . . . 9 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔𝐵) → ∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟))
164163ex 413 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔𝐵 → ∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
165 eliun 4929 . . . . . . . 8 (𝑔 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦X 𝑥𝐼 (𝑓𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟))
166164, 165syl6ibr 251 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔𝐵𝑔 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟)))
167166ssrdv 3928 . . . . . 6 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐵 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟))
16882, 167eqssd 3939 . . . . 5 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵)
169 iuneq1 4941 . . . . . . 7 (𝑣 = X𝑥𝐼 (𝑓𝑥) → 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟))
170169eqeq1d 2741 . . . . . 6 (𝑣 = X𝑥𝐼 (𝑓𝑥) → ( 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵))
171170rspcev 3562 . . . . 5 ((X𝑥𝐼 (𝑓𝑥) ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦X 𝑥𝐼 (𝑓𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
17269, 168, 171syl2anc 584 . . . 4 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥𝐼 ((𝑓𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝑧 ∈ (𝑓𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
17343, 172exlimddv 1939 . . 3 ((𝜑𝑟 ∈ ℝ+) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
174173ralrimiva 3104 . 2 (𝜑 → ∀𝑟 ∈ ℝ+𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
175 istotbnd3 35938 . 2 (𝐷 ∈ (TotBnd‘𝐵) ↔ (𝐷 ∈ (Met‘𝐵) ∧ ∀𝑟 ∈ ℝ+𝑣 ∈ (𝒫 𝐵 ∩ Fin) 𝑦𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵))
17626, 174, 175sylanbrc 583 1 (𝜑𝐷 ∈ (TotBnd‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1539  wex 1782  wcel 2107  wral 3065  wrex 3066  Vcvv 3433  cin 3887  wss 3888  𝒫 cpw 4534   ciun 4925   class class class wbr 5075  cmpt 5158   × cxp 5588  cres 5592   Fn wfn 6432  wf 6433  cfv 6437  (class class class)co 7284  Xcixp 8694  Fincfn 8742  0cc0 10880  *cxr 11017   < clt 11018  +crp 12739  Basecbs 16921  distcds 16980  Xscprds 17165  ∞Metcxmet 20591  Metcmet 20592  ballcbl 20593  TotBndctotbnd 35933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-er 8507  df-map 8626  df-pm 8627  df-ixp 8695  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-sup 9210  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-4 12047  df-5 12048  df-6 12049  df-7 12050  df-8 12051  df-9 12052  df-n0 12243  df-z 12329  df-dec 12447  df-uz 12592  df-rp 12740  df-xneg 12857  df-xadd 12858  df-xmul 12859  df-icc 13095  df-fz 13249  df-struct 16857  df-slot 16892  df-ndx 16904  df-base 16922  df-plusg 16984  df-mulr 16985  df-sca 16987  df-vsca 16988  df-ip 16989  df-tset 16990  df-ple 16991  df-ds 16993  df-hom 16995  df-cco 16996  df-prds 17167  df-psmet 20598  df-xmet 20599  df-met 20600  df-bl 20601  df-totbnd 35935
This theorem is referenced by:  prdsbnd2  35962
  Copyright terms: Public domain W3C validator