Metamath Proof Explorer

Theorem prdstotbnd

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)

Ref Expression
Hypotheses 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 prdstotbnd ( 𝜑 → 𝐷 ∈ ( TotBnd ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 prdsbnd.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsbnd.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 prdsbnd.v ⊢ 𝑉 = ( Base ‘ ( 𝑅 ‘ 𝑥 ) )
4 prdsbnd.e ⊢ 𝐸 = ( ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ↾ ( 𝑉 × 𝑉 ) )
5 prdsbnd.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
6 prdsbnd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
7 prdsbnd.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
8 prdsbnd.r ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
9 prdstotbnd.m ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( TotBnd ‘ 𝑉 ) )
10 eqid ⊢ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) )
11 eqid ⊢ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) )
12 eqid ⊢ ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) = ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) )
13 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ V )
14 totbndmet ⊢ ( 𝐸 ∈ ( TotBnd ‘ 𝑉 ) → 𝐸 ∈ ( Met ‘ 𝑉 ) )
15 9 14 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( Met ‘ 𝑉 ) )
16 10 11 3 4 12 6 7 13 15 prdsmet ⊢ ( 𝜑 → ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) ) )
17 dffn5 ⊢ ( 𝑅 Fn 𝐼 ↔ 𝑅 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) )
18 8 17 sylib ⊢ ( 𝜑 → 𝑅 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) )
19 18 oveq2d ⊢ ( 𝜑 → ( 𝑆 Xs 𝑅 ) = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) )
20 1 19 eqtrid ⊢ ( 𝜑 → 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) )
21 20 fveq2d ⊢ ( 𝜑 → ( dist ‘ 𝑌 ) = ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
22 5 21 eqtrid ⊢ ( 𝜑 → 𝐷 = ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
23 20 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
24 2 23 eqtrid ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
25 24 fveq2d ⊢ ( 𝜑 → ( Met ‘ 𝐵 ) = ( Met ‘ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) ) )
26 16 22 25 3eltr4d ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝐵 ) )
27 7 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝐼 ∈ Fin )
28 istotbnd3 ⊢ ( 𝐸 ∈ ( TotBnd ‘ 𝑉 ) ↔ ( 𝐸 ∈ ( Met ‘ 𝑉 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) )
29 28 simprbi ⊢ ( 𝐸 ∈ ( TotBnd ‘ 𝑉 ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 )
30 9 29 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 )
31 30 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 )
32 df-rex ⊢ ( ∃ 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ↔ ∃ 𝑤 ( 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) )
33 rexv ⊢ ( ∃ 𝑤 ∈ V ( 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ↔ ∃ 𝑤 ( 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) )
34 32 33 bitr4i ⊢ ( ∃ 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ↔ ∃ 𝑤 ∈ V ( 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) )
35 31 34 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑤 ∈ V ( 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) )
36 35 an32s ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐼 ) → ∃ 𝑤 ∈ V ( 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) )
37 36 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑥 ∈ 𝐼 ∃ 𝑤 ∈ V ( 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) )
38 eleq1 ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑥 ) → ( 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ) )
39 iuneq1 ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑥 ) → ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) )
40 39 eqeq1d ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑥 ) → ( ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ↔ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) )
41 38 40 anbi12d ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑥 ) → ( ( 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ↔ ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) )
42 41 ac6sfi ⊢ ( ( 𝐼 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐼 ∃ 𝑤 ∈ V ( 𝑤 ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ 𝑤 ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) → ∃ 𝑓 ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) )
43 27 37 42 syl2anc ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑓 ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) )
44 elfpw ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ↔ ( ( 𝑓 ‘ 𝑥 ) ⊆ 𝑉 ∧ ( 𝑓 ‘ 𝑥 ) ∈ Fin ) )
45 44 simplbi ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) → ( 𝑓 ‘ 𝑥 ) ⊆ 𝑉 )
46 45 adantr ⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) → ( 𝑓 ‘ 𝑥 ) ⊆ 𝑉 )
47 46 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) → ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ⊆ 𝑉 )
48 47 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ⊆ 𝑉 )
49 ss2ixp ⊢ ( ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ⊆ 𝑉 → X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ⊆ X 𝑥 ∈ 𝐼 𝑉 )
50 48 49 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ⊆ X 𝑥 ∈ 𝐼 𝑉 )
51 fnfi ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) → 𝑅 ∈ Fin )
52 8 7 51 syl2anc ⊢ ( 𝜑 → 𝑅 ∈ Fin )
53 8 fndmd ⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
54 1 6 52 2 53 prdsbas ⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
55 3 rgenw ⊢ ∀ 𝑥 ∈ 𝐼 𝑉 = ( Base ‘ ( 𝑅 ‘ 𝑥 ) )
56 ixpeq2 ⊢ ( ∀ 𝑥 ∈ 𝐼 𝑉 = ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) → X 𝑥 ∈ 𝐼 𝑉 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
57 55 56 ax-mp ⊢ X 𝑥 ∈ 𝐼 𝑉 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) )
58 54 57 eqtr4di ⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 𝑉 )
59 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → 𝐵 = X 𝑥 ∈ 𝐼 𝑉 )
60 50 59 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ⊆ 𝐵 )
61 27 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → 𝐼 ∈ Fin )
62 44 simprbi ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) → ( 𝑓 ‘ 𝑥 ) ∈ Fin )
63 62 adantr ⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) → ( 𝑓 ‘ 𝑥 ) ∈ Fin )
64 63 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) → ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ Fin )
65 64 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ Fin )
66 ixpfi ⊢ ( ( 𝐼 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ Fin ) → X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ Fin )
67 61 65 66 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ Fin )
68 elfpw ⊢ ( X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝐵 ∩ Fin ) ↔ ( X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ⊆ 𝐵 ∧ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ Fin ) )
69 60 67 68 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝐵 ∩ Fin ) )
70 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝐵 ) → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
71 26 70 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
72 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
73 blssm ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 )
74 73 3expa ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑟 ∈ ℝ* ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 )
75 74 an32s ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑟 ∈ ℝ* ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 )
76 75 ralrimiva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑟 ∈ ℝ* ) → ∀ 𝑦 ∈ 𝐵 ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 )
77 71 72 76 syl2an ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑦 ∈ 𝐵 ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 )
78 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → ∀ 𝑦 ∈ 𝐵 ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 )
79 ssralv ⊢ ( X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ⊆ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 → ∀ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 ) )
80 60 78 79 sylc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → ∀ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 )
81 iunss ⊢ ( ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 ↔ ∀ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 )
82 80 81 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 )
83 61 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) → 𝐼 ∈ Fin )
84 59 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → ( 𝑔 ∈ 𝐵 ↔ 𝑔 ∈ X 𝑥 ∈ 𝐼 𝑉 ) )
85 vex ⊢ 𝑔 ∈ V
86 85 elixp ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐼 𝑉 ↔ ( 𝑔 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) )
87 86 simprbi ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐼 𝑉 → ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 )
88 df-rex ⊢ ( ∃ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ↔ ∃ 𝑧 ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) )
89 eliun ⊢ ( ( 𝑔 ‘ 𝑥 ) ∈ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ↔ ∃ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) )
90 rexv ⊢ ( ∃ 𝑧 ∈ V ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) ↔ ∃ 𝑧 ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) )
91 88 89 90 3bitr4i ⊢ ( ( 𝑔 ‘ 𝑥 ) ∈ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ↔ ∃ 𝑧 ∈ V ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) )
92 eleq2 ⊢ ( ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 → ( ( 𝑔 ‘ 𝑥 ) ∈ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ↔ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) )
93 91 92 bitr3id ⊢ ( ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 → ( ∃ 𝑧 ∈ V ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) ↔ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) )
94 93 biimprd ⊢ ( ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 → ( ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 → ∃ 𝑧 ∈ V ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
95 94 adantl ⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) → ( ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 → ∃ 𝑧 ∈ V ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
96 95 ral2imi ⊢ ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 → ∀ 𝑥 ∈ 𝐼 ∃ 𝑧 ∈ V ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
97 96 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 → ∀ 𝑥 ∈ 𝐼 ∃ 𝑧 ∈ V ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
98 87 97 syl5 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → ( 𝑔 ∈ X 𝑥 ∈ 𝐼 𝑉 → ∀ 𝑥 ∈ 𝐼 ∃ 𝑧 ∈ V ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
99 84 98 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → ( 𝑔 ∈ 𝐵 → ∀ 𝑥 ∈ 𝐼 ∃ 𝑧 ∈ V ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
100 99 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐼 ∃ 𝑧 ∈ V ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) )
101 eleq1 ⊢ ( 𝑧 = ( 𝑦 ‘ 𝑥 ) → ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ↔ ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ) )
102 oveq1 ⊢ ( 𝑧 = ( 𝑦 ‘ 𝑥 ) → ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) )
103 102 eleq2d ⊢ ( 𝑧 = ( 𝑦 ‘ 𝑥 ) → ( ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ↔ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
104 101 103 anbi12d ⊢ ( 𝑧 = ( 𝑦 ‘ 𝑥 ) → ( ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) ↔ ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
105 104 ac6sfi ⊢ ( ( 𝐼 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐼 ∃ 𝑧 ∈ V ( 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) ) ) → ∃ 𝑦 ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
106 83 100 105 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) → ∃ 𝑦 ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
107 ffn ⊢ ( 𝑦 : 𝐼 ⟶ V → 𝑦 Fn 𝐼 )
108 simpl ⊢ ( ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) → ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) )
109 108 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) )
110 107 109 anim12i ⊢ ( ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) → ( 𝑦 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ) )
111 vex ⊢ 𝑦 ∈ V
112 111 elixp ⊢ ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ↔ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ) )
113 110 112 sylibr ⊢ ( ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) → 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) )
114 113 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) → 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) )
115 84 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ X 𝑥 ∈ 𝐼 𝑉 )
116 ixpfn ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐼 𝑉 → 𝑔 Fn 𝐼 )
117 115 116 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) → 𝑔 Fn 𝐼 )
118 117 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) → 𝑔 Fn 𝐼 )
119 simpr ⊢ ( ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) → ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) )
120 119 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) )
121 120 ad2antll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) )
122 85 elixp ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ↔ ( 𝑔 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
123 118 121 122 sylanbrc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) → 𝑔 ∈ X 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) )
124 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) → 𝜑 )
125 50 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) → X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ⊆ X 𝑥 ∈ 𝐼 𝑉 )
126 125 114 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) → 𝑦 ∈ X 𝑥 ∈ 𝐼 𝑉 )
127 124 58 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) → 𝐵 = X 𝑥 ∈ 𝐼 𝑉 )
128 126 127 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) → 𝑦 ∈ 𝐵 )
129 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) → 𝑟 ∈ ℝ+ )
130 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑅 ‘ 𝑦 ) = ( 𝑅 ‘ 𝑥 ) )
131 130 cbvmptv ⊢ ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) )
132 131 oveq2i ⊢ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) )
133 20 132 eqtr4di ⊢ ( 𝜑 → 𝑌 = ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) )
134 133 fveq2d ⊢ ( 𝜑 → ( dist ‘ 𝑌 ) = ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) )
135 5 134 eqtrid ⊢ ( 𝜑 → 𝐷 = ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) )
136 135 fveq2d ⊢ ( 𝜑 → ( ball ‘ 𝐷 ) = ( ball ‘ ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) ) )
137 136 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = ( 𝑦 ( ball ‘ ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) )
138 eqid ⊢ ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) )
139 eqid ⊢ ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) = ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) )
140 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑆 ∈ 𝑊 )
141 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝐼 ∈ Fin )
142 fvexd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ V )
143 metxmet ⊢ ( 𝐸 ∈ ( Met ‘ 𝑉 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
144 15 143 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
145 144 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
146 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑦 ∈ 𝐵 )
147 133 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) )
148 2 147 eqtrid ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) )
149 148 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) )
150 146 149 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑦 ∈ ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) )
151 72 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ* )
152 rpgt0 ⊢ ( 𝑟 ∈ ℝ+ → 0 < 𝑟 )
153 152 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 0 < 𝑟 )
154 132 138 3 4 139 140 141 142 145 150 151 153 prdsbl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑦 ( ball ‘ ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) = X 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) )
155 137 154 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) )
156 124 128 129 155 syl12anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) )
157 123 156 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) → 𝑔 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
158 114 157 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) → ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∧ 𝑔 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
159 158 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) → ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∧ 𝑔 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
160 159 eximdv ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) → ( ∃ 𝑦 ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) → ∃ 𝑦 ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∧ 𝑔 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
161 df-rex ⊢ ( ∃ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) 𝑔 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ↔ ∃ 𝑦 ( 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∧ 𝑔 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
162 160 161 imbitrrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) → ( ∃ 𝑦 ( 𝑦 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑦 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( ( 𝑦 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) → ∃ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) 𝑔 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
163 106 162 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) ∧ 𝑔 ∈ 𝐵 ) → ∃ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) 𝑔 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
164 163 ex ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → ( 𝑔 ∈ 𝐵 → ∃ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) 𝑔 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
165 eliun ⊢ ( 𝑔 ∈ ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ↔ ∃ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) 𝑔 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
166 164 165 imbitrrdi ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → ( 𝑔 ∈ 𝐵 → 𝑔 ∈ ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
167 166 ssrdv ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → 𝐵 ⊆ ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
168 82 167 eqssd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = 𝐵 )
169 iuneq1 ⊢ ( 𝑣 = X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) → ∪ 𝑦 ∈ 𝑣 ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
170 169 eqeq1d ⊢ ( 𝑣 = X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) → ( ∪ 𝑦 ∈ 𝑣 ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = 𝐵 ↔ ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = 𝐵 ) )
171 170 rspcev ⊢ ( ( X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = 𝐵 ) → ∃ 𝑣 ∈ ( 𝒫 𝐵 ∩ Fin ) ∪ 𝑦 ∈ 𝑣 ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = 𝐵 )
172 69 168 171 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 : 𝐼 ⟶ V ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ∧ ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑥 ) ( 𝑧 ( ball ‘ 𝐸 ) 𝑟 ) = 𝑉 ) ) ) → ∃ 𝑣 ∈ ( 𝒫 𝐵 ∩ Fin ) ∪ 𝑦 ∈ 𝑣 ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = 𝐵 )
173 43 172 exlimddv ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑣 ∈ ( 𝒫 𝐵 ∩ Fin ) ∪ 𝑦 ∈ 𝑣 ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = 𝐵 )
174 173 ralrimiva ⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝐵 ∩ Fin ) ∪ 𝑦 ∈ 𝑣 ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = 𝐵 )
175 istotbnd3 ⊢ ( 𝐷 ∈ ( TotBnd ‘ 𝐵 ) ↔ ( 𝐷 ∈ ( Met ‘ 𝐵 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝐵 ∩ Fin ) ∪ 𝑦 ∈ 𝑣 ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = 𝐵 ) )
176 26 174 175 sylanbrc ⊢ ( 𝜑 → 𝐷 ∈ ( TotBnd ‘ 𝐵 ) )