Metamath Proof Explorer

Theorem prdsbnd2

Description: If balls are totally bounded in each factor, then balls are bounded in a metric product. (Contributed by Mario Carneiro, 16-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 𝐼 )
prdsbnd2.c ⊢ 𝐶 = ( 𝐷 ↾ ( 𝐴 × 𝐴 ) )
prdsbnd2.e ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( Met ‘ 𝑉 ) )
prdsbnd2.m ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐸 ↾ ( 𝑦 × 𝑦 ) ) ∈ ( TotBnd ‘ 𝑦 ) ↔ ( 𝐸 ↾ ( 𝑦 × 𝑦 ) ) ∈ ( Bnd ‘ 𝑦 ) ) )
Assertion prdsbnd2 ( 𝜑 → ( 𝐶 ∈ ( TotBnd ‘ 𝐴 ) ↔ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) )

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 prdsbnd2.c ⊢ 𝐶 = ( 𝐷 ↾ ( 𝐴 × 𝐴 ) )
10 prdsbnd2.e ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( Met ‘ 𝑉 ) )
11 prdsbnd2.m ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐸 ↾ ( 𝑦 × 𝑦 ) ) ∈ ( TotBnd ‘ 𝑦 ) ↔ ( 𝐸 ↾ ( 𝑦 × 𝑦 ) ) ∈ ( Bnd ‘ 𝑦 ) ) )
12 totbndbnd ⊢ ( 𝐶 ∈ ( TotBnd ‘ 𝐴 ) → 𝐶 ∈ ( Bnd ‘ 𝐴 ) )
13 bndmet ⊢ ( 𝐶 ∈ ( Bnd ‘ 𝐴 ) → 𝐶 ∈ ( Met ‘ 𝐴 ) )
14 0totbnd ⊢ ( 𝐴 = ∅ → ( 𝐶 ∈ ( TotBnd ‘ 𝐴 ) ↔ 𝐶 ∈ ( Met ‘ 𝐴 ) ) )
15 13 14 imbitrrid ⊢ ( 𝐴 = ∅ → ( 𝐶 ∈ ( Bnd ‘ 𝐴 ) → 𝐶 ∈ ( TotBnd ‘ 𝐴 ) ) )
16 15 a1i ⊢ ( 𝜑 → ( 𝐴 = ∅ → ( 𝐶 ∈ ( Bnd ‘ 𝐴 ) → 𝐶 ∈ ( TotBnd ‘ 𝐴 ) ) ) )
17 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑎 𝑎 ∈ 𝐴 )
18 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) → 𝐶 ∈ ( Bnd ‘ 𝐴 ) )
19 eqid ⊢ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) )
20 eqid ⊢ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) )
21 eqid ⊢ ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) = ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) )
22 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ V )
23 19 20 3 4 21 6 7 22 10 prdsmet ⊢ ( 𝜑 → ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) ) )
24 dffn5 ⊢ ( 𝑅 Fn 𝐼 ↔ 𝑅 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) )
25 8 24 sylib ⊢ ( 𝜑 → 𝑅 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) )
26 25 oveq2d ⊢ ( 𝜑 → ( 𝑆 Xs 𝑅 ) = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) )
27 1 26 eqtrid ⊢ ( 𝜑 → 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) )
28 27 fveq2d ⊢ ( 𝜑 → ( dist ‘ 𝑌 ) = ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
29 5 28 eqtrid ⊢ ( 𝜑 → 𝐷 = ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
30 27 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
31 2 30 eqtrid ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
32 31 fveq2d ⊢ ( 𝜑 → ( Met ‘ 𝐵 ) = ( Met ‘ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) ) )
33 23 29 32 3eltr4d ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝐵 ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) → 𝐷 ∈ ( Met ‘ 𝐵 ) )
35 simpr ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) → 𝐶 ∈ ( Bnd ‘ 𝐴 ) )
36 9 bnd2lem ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝐵 ) ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) → 𝐴 ⊆ 𝐵 )
37 33 35 36 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) → 𝐴 ⊆ 𝐵 )
38 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) → 𝑎 ∈ 𝐴 )
39 37 38 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) → 𝑎 ∈ 𝐵 )
40 9 ssbnd ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → ( 𝐶 ∈ ( Bnd ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ ℝ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) )
41 34 39 40 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) → ( 𝐶 ∈ ( Bnd ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ ℝ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) )
42 18 41 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) → ∃ 𝑟 ∈ ℝ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) )
43 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) )
44 xpss12 ⊢ ( ( 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( 𝐴 × 𝐴 ) ⊆ ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) × ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) )
45 43 43 44 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → ( 𝐴 × 𝐴 ) ⊆ ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) × ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) )
46 45 resabs1d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → ( ( 𝐷 ↾ ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) × ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( 𝐷 ↾ ( 𝐴 × 𝐴 ) ) )
47 46 9 eqtr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → ( ( 𝐷 ↾ ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) × ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) = 𝐶 )
48 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → 𝜑 )
49 39 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → 𝑎 ∈ 𝐵 )
50 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → 𝑟 ∈ ℝ )
51 38 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → 𝑎 ∈ 𝐴 )
52 43 51 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → 𝑎 ∈ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) )
53 52 ne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ≠ ∅ )
54 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → 𝐷 ∈ ( Met ‘ 𝐵 ) )
55 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝐵 ) → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
56 54 55 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
57 50 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → 𝑟 ∈ ℝ* )
58 xbln0 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) → ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ≠ ∅ ↔ 0 < 𝑟 ) )
59 56 49 57 58 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ≠ ∅ ↔ 0 < 𝑟 ) )
60 53 59 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → 0 < 𝑟 )
61 50 60 elrpd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → 𝑟 ∈ ℝ+ )
62 eqid ⊢ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) = ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) )
63 eqid ⊢ ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) )
64 eqid ⊢ ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) = ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) )
65 eqid ⊢ ( ( dist ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) ↾ ( ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) × ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) ) ) = ( ( dist ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) ↾ ( ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) × ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) ) )
66 eqid ⊢ ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) ) = ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) )
67 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑆 ∈ 𝑊 )
68 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝐼 ∈ Fin )
69 ovex ⊢ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ∈ V
70 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑅 ‘ 𝑦 ) = ( 𝑅 ‘ 𝑥 ) )
71 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) = ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) )
72 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
73 72 3 eqtr4di ⊢ ( 𝑦 = 𝑥 → ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) = 𝑉 )
74 73 sqxpeqd ⊢ ( 𝑦 = 𝑥 → ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( 𝑉 × 𝑉 ) )
75 71 74 reseq12d ⊢ ( 𝑦 = 𝑥 → ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) = ( ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ↾ ( 𝑉 × 𝑉 ) ) )
76 75 4 eqtr4di ⊢ ( 𝑦 = 𝑥 → ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) = 𝐸 )
77 76 fveq2d ⊢ ( 𝑦 = 𝑥 → ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) = ( ball ‘ 𝐸 ) )
78 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑎 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑥 ) )
79 eqidd ⊢ ( 𝑦 = 𝑥 → 𝑟 = 𝑟 )
80 77 78 79 oveq123d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) = ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) )
81 70 80 oveq12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) = ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
82 81 cbvmptv ⊢ ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
83 69 82 fnmpti ⊢ ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) Fn 𝐼
84 83 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) Fn 𝐼 )
85 10 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( Met ‘ 𝑉 ) )
86 metxmet ⊢ ( 𝐸 ∈ ( Met ‘ 𝑉 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
87 85 86 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
88 22 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝑅 ‘ 𝑥 ) ∈ V )
89 88 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑅 ‘ 𝑥 ) ∈ V )
90 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑎 ∈ 𝐵 )
91 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
92 90 91 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑎 ∈ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) ) )
93 19 20 67 68 89 3 92 prdsbascl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑎 ‘ 𝑥 ) ∈ 𝑉 )
94 93 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑥 ) ∈ 𝑉 )
95 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑟 ∈ ℝ+ )
96 95 rpred ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑟 ∈ ℝ )
97 blbnd ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( 𝑎 ‘ 𝑥 ) ∈ 𝑉 ∧ 𝑟 ∈ ℝ ) → ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ∈ ( Bnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
98 87 94 96 97 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ∈ ( Bnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
99 ovex ⊢ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ∈ V
100 xpeq12 ⊢ ( ( 𝑦 = ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ∧ 𝑦 = ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) → ( 𝑦 × 𝑦 ) = ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
101 100 anidms ⊢ ( 𝑦 = ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) → ( 𝑦 × 𝑦 ) = ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
102 101 reseq2d ⊢ ( 𝑦 = ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) → ( 𝐸 ↾ ( 𝑦 × 𝑦 ) ) = ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
103 fveq2 ⊢ ( 𝑦 = ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) → ( TotBnd ‘ 𝑦 ) = ( TotBnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
104 102 103 eleq12d ⊢ ( 𝑦 = ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) → ( ( 𝐸 ↾ ( 𝑦 × 𝑦 ) ) ∈ ( TotBnd ‘ 𝑦 ) ↔ ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ∈ ( TotBnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
105 fveq2 ⊢ ( 𝑦 = ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) → ( Bnd ‘ 𝑦 ) = ( Bnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
106 102 105 eleq12d ⊢ ( 𝑦 = ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) → ( ( 𝐸 ↾ ( 𝑦 × 𝑦 ) ) ∈ ( Bnd ‘ 𝑦 ) ↔ ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ∈ ( Bnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
107 104 106 bibi12d ⊢ ( 𝑦 = ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) → ( ( ( 𝐸 ↾ ( 𝑦 × 𝑦 ) ) ∈ ( TotBnd ‘ 𝑦 ) ↔ ( 𝐸 ↾ ( 𝑦 × 𝑦 ) ) ∈ ( Bnd ‘ 𝑦 ) ) ↔ ( ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ∈ ( TotBnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ↔ ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ∈ ( Bnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) )
108 107 imbi2d ⊢ ( 𝑦 = ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐸 ↾ ( 𝑦 × 𝑦 ) ) ∈ ( TotBnd ‘ 𝑦 ) ↔ ( 𝐸 ↾ ( 𝑦 × 𝑦 ) ) ∈ ( Bnd ‘ 𝑦 ) ) ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ∈ ( TotBnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ↔ ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ∈ ( Bnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) ) )
109 99 108 11 vtocl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ∈ ( TotBnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ↔ ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ∈ ( Bnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
110 109 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ∈ ( TotBnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ↔ ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ∈ ( Bnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
111 98 110 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ∈ ( TotBnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
112 eqid ⊢ ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) )
113 81 112 69 fvmpt ⊢ ( 𝑥 ∈ 𝐼 → ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) = ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
114 113 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) = ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
115 114 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( dist ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) = ( dist ‘ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
116 eqid ⊢ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) = ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) )
117 eqid ⊢ ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) = ( dist ‘ ( 𝑅 ‘ 𝑥 ) )
118 116 117 ressds ⊢ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ∈ V → ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) = ( dist ‘ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
119 99 118 ax-mp ⊢ ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) = ( dist ‘ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
120 115 119 eqtr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( dist ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) = ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) )
121 114 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) = ( Base ‘ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
122 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
123 122 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ* )
124 123 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑟 ∈ ℝ* )
125 blssm ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( 𝑎 ‘ 𝑥 ) ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) → ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑉 )
126 87 94 124 125 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑉 )
127 116 3 ressbas2 ⊢ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑉 → ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) = ( Base ‘ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
128 126 127 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) = ( Base ‘ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
129 121 128 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) = ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) )
130 129 sqxpeqd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) × ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) ) = ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
131 120 130 reseq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( dist ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) ↾ ( ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) × ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) ) ) = ( ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
132 4 reseq1i ⊢ ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) = ( ( ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ↾ ( 𝑉 × 𝑉 ) ) ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
133 xpss12 ⊢ ( ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑉 ∧ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑉 ) → ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ⊆ ( 𝑉 × 𝑉 ) )
134 126 126 133 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ⊆ ( 𝑉 × 𝑉 ) )
135 134 resabs1d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ↾ ( 𝑉 × 𝑉 ) ) ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) = ( ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
136 132 135 eqtrid ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) = ( ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
137 131 136 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( dist ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) ↾ ( ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) × ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) ) ) = ( 𝐸 ↾ ( ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) × ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
138 129 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( TotBnd ‘ ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) ) = ( TotBnd ‘ ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
139 111 137 138 3eltr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( dist ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) ↾ ( ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) × ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) ) ) ∈ ( TotBnd ‘ ( Base ‘ ( ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ‘ 𝑥 ) ) ) )
140 62 63 64 65 66 67 68 84 139 prdstotbnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) ) ∈ ( TotBnd ‘ ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) ) ) )
141 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) ) )
142 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) )
143 eqid ⊢ ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) )
144 82 oveq2i ⊢ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
145 144 fveq2i ⊢ ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) ) = ( dist ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) )
146 fvexd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ V )
147 99 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ∈ V )
148 141 142 143 5 145 67 67 68 146 147 ressprdsds ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) ) = ( 𝐷 ↾ ( ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) ) × ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) ) ) ) )
149 128 ixpeq2dva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → X 𝑥 ∈ 𝐼 ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
150 70 cbvmptv ⊢ ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) )
151 150 oveq2i ⊢ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑥 ) ) )
152 27 151 eqtr4di ⊢ ( 𝜑 → 𝑌 = ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) )
153 152 fveq2d ⊢ ( 𝜑 → ( dist ‘ 𝑌 ) = ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) )
154 5 153 eqtrid ⊢ ( 𝜑 → 𝐷 = ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) )
155 154 fveq2d ⊢ ( 𝜑 → ( ball ‘ 𝐷 ) = ( ball ‘ ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) ) )
156 155 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) = ( 𝑎 ( ball ‘ ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) )
157 eqid ⊢ ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) )
158 eqid ⊢ ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) = ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) )
159 152 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) )
160 2 159 eqtrid ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) )
161 160 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) )
162 90 161 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑎 ∈ ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) )
163 rpgt0 ⊢ ( 𝑟 ∈ ℝ+ → 0 < 𝑟 )
164 163 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → 0 < 𝑟 )
165 151 157 3 4 158 67 68 146 87 162 123 164 prdsbl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑎 ( ball ‘ ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) = X 𝑥 ∈ 𝐼 ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) )
166 156 165 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑥 ∈ 𝐼 ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) )
167 eqid ⊢ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
168 69 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ∈ V )
169 168 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ∈ V )
170 eqid ⊢ ( Base ‘ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) = ( Base ‘ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) )
171 167 143 67 68 169 170 prdsbas3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) )
172 149 166 171 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) ) = ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) )
173 172 sqxpeqd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) ) × ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) ) ) = ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) × ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) )
174 173 reseq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝐷 ↾ ( ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) ) × ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) ) ) ) = ( 𝐷 ↾ ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) × ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
175 148 174 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( dist ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) ) = ( 𝐷 ↾ ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) × ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
176 144 fveq2i ⊢ ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑥 ) ↾s ( ( 𝑎 ‘ 𝑥 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) )
177 176 172 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) ) = ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) )
178 177 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( TotBnd ‘ ( Base ‘ ( 𝑆 Xs ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑅 ‘ 𝑦 ) ↾s ( ( 𝑎 ‘ 𝑦 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑦 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) ) 𝑟 ) ) ) ) ) ) = ( TotBnd ‘ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) )
179 140 175 178 3eltr3d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝐷 ↾ ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) × ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) ∈ ( TotBnd ‘ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) )
180 48 49 61 179 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → ( 𝐷 ↾ ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) × ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) ∈ ( TotBnd ‘ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) )
181 totbndss ⊢ ( ( ( 𝐷 ↾ ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) × ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) ∈ ( TotBnd ‘ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( ( 𝐷 ↾ ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) × ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( TotBnd ‘ 𝐴 ) )
182 180 43 181 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → ( ( 𝐷 ↾ ( ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) × ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( TotBnd ‘ 𝐴 ) )
183 47 182 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ ℝ ∧ 𝐴 ⊆ ( 𝑎 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → 𝐶 ∈ ( TotBnd ‘ 𝐴 ) )
184 42 183 rexlimddv ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) ) → 𝐶 ∈ ( TotBnd ‘ 𝐴 ) )
185 184 exp32 ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐴 → ( 𝐶 ∈ ( Bnd ‘ 𝐴 ) → 𝐶 ∈ ( TotBnd ‘ 𝐴 ) ) ) )
186 185 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑎 𝑎 ∈ 𝐴 → ( 𝐶 ∈ ( Bnd ‘ 𝐴 ) → 𝐶 ∈ ( TotBnd ‘ 𝐴 ) ) ) )
187 17 186 biimtrid ⊢ ( 𝜑 → ( 𝐴 ≠ ∅ → ( 𝐶 ∈ ( Bnd ‘ 𝐴 ) → 𝐶 ∈ ( TotBnd ‘ 𝐴 ) ) ) )
188 16 187 pm2.61dne ⊢ ( 𝜑 → ( 𝐶 ∈ ( Bnd ‘ 𝐴 ) → 𝐶 ∈ ( TotBnd ‘ 𝐴 ) ) )
189 12 188 impbid2 ⊢ ( 𝜑 → ( 𝐶 ∈ ( TotBnd ‘ 𝐴 ) ↔ 𝐶 ∈ ( Bnd ‘ 𝐴 ) ) )