prdsbnd2 - Mathbox for Jeff Madsen

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

Theorem prdsbnd2 36966

Description: If balls are totally bounded in each factor, then balls are bounded in a metric product. (Contributed by Mario Carneiro, 16-Sep-2015.)

**Hypotheses**
Ref	Expression
prdsbnd.y	⊢ 𝑌 = (𝑆X_s𝑅)
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**
Ref	Expression
prdsbnd2	⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Bnd‘𝐴)))

Distinct variable groups: 𝑦,𝐷 𝑥,𝑦,𝑅 𝑥,𝐵,𝑦 𝑦,𝐸 𝜑,𝑥,𝑦 𝑥,𝐼,𝑦 𝑥,𝑆 𝑦,𝑉 𝑥,𝑌 Allowed substitution hints: 𝐴(𝑥,𝑦) 𝐶(𝑥,𝑦) 𝐷(𝑥) 𝑆(𝑦) 𝐸(𝑥) 𝑉(𝑥) 𝑊(𝑥,𝑦) 𝑌(𝑦)

Proof of Theorem prdsbnd2 Dummy variables 𝑟 𝑎 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		totbndbnd 36960	. 2 ⊢ (𝐶 ∈ (TotBnd‘𝐴) → 𝐶 ∈ (Bnd‘𝐴))
2		bndmet 36952	. . . . 5 ⊢ (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (Met‘𝐴))
3		0totbnd 36944	. . . . 5 ⊢ (𝐴 = ∅ → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Met‘𝐴)))
4	2, 3	imbitrrid 245	. . . 4 ⊢ (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))
5	4	a1i 11	. . 3 ⊢ (𝜑 → (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
6		n0 4345	. . . 4 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑎 𝑎 ∈ 𝐴)
7		simprr 769	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (Bnd‘𝐴))
8		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
9		eqid 2730	. . . . . . . . . . . 12 ⊢ (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
10		prdsbnd.v	. . . . . . . . . . . 12 ⊢ 𝑉 = (Base‘(𝑅‘𝑥))
11		prdsbnd.e	. . . . . . . . . . . 12 ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉))
12		eqid 2730	. . . . . . . . . . . 12 ⊢ (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
13		prdsbnd.s	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ 𝑊)
14		prdsbnd.i	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ Fin)
15		fvexd 6905	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V)
16		prdsbnd2.e	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉))
17	8, 9, 10, 11, 12, 13, 14, 15, 16	prdsmet 24096	. . . . . . . . . . 11 ⊢ (𝜑 → (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) ∈ (Met‘(Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))))
18		prdsbnd.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (dist‘𝑌)
19		prdsbnd.y	. . . . . . . . . . . . . 14 ⊢ 𝑌 = (𝑆X_s𝑅)
20		prdsbnd.r	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑅 Fn 𝐼)
21		dffn5 6949	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 Fn 𝐼 ↔ 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
22	20, 21	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
23	22	oveq2d 7427	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆X_s𝑅) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
24	19, 23	eqtrid 2782	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
25	24	fveq2d 6894	. . . . . . . . . . . 12 ⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
26	18, 25	eqtrid 2782	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
27		prdsbnd.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝑌)
28	24	fveq2d 6894	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
29	27, 28	eqtrid 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
30	29	fveq2d 6894	. . . . . . . . . . 11 ⊢ (𝜑 → (Met‘𝐵) = (Met‘(Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))))
31	17, 26, 30	3eltr4d 2846	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵))
32	31	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐷 ∈ (Met‘𝐵))
33		simpr 483	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐶 ∈ (Bnd‘𝐴))
34		prdsbnd2.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (𝐷 ↾ (𝐴 × 𝐴))
35	34	bnd2lem 36962	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐴 ⊆ 𝐵)
36	31, 33, 35	syl2an 594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐴 ⊆ 𝐵)
37		simprl 767	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐴)
38	36, 37	sseldd 3982	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐵)
39	34	ssbnd 36959	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝑎 ∈ 𝐵) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)))
40	32, 38, 39	syl2anc 582	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)))
41	7, 40	mpbid 231	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))
42		simprr 769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))
43		xpss12 5690	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ (𝑎(ball‘𝐷)𝑟) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
44	42, 42, 43	syl2anc 582	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
45	44	resabs1d 6011	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = (𝐷 ↾ (𝐴 × 𝐴)))
46	45, 34	eqtr4di 2788	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = 𝐶)
47		simpll 763	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝜑)
48	38	adantr 479	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐵)
49		simprl 767	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ)
50	37	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐴)
51	42, 50	sseldd 3982	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ (𝑎(ball‘𝐷)𝑟))
52	51	ne0d 4334	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝑎(ball‘𝐷)𝑟) ≠ ∅)
53	31	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (Met‘𝐵))
54		metxmet 24060	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵))
55	53, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (∞Met‘𝐵))
56	49	rexrd 11268	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ^*)
57		xbln0 24140	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^*) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
58	55, 48, 56, 57	syl3anc 1369	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
59	52, 58	mpbid 231	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 0 < 𝑟)
60	49, 59	elrpd 13017	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ⁺)
61		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))
62		eqid 2730	. . . . . . . . . . . 12 ⊢ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))
63		eqid 2730	. . . . . . . . . . . 12 ⊢ (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))
64		eqid 2730	. . . . . . . . . . . 12 ⊢ ((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‘(𝑅‘𝑦)))))𝑟)))‘𝑥))))
65		eqid 2730	. . . . . . . . . . . 12 ⊢ (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))
66	13	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑆 ∈ 𝑊)
67	14	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝐼 ∈ Fin)
68		ovex 7444	. . . . . . . . . . . . . 14 ⊢ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V
69		fveq2 6890	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥))
70		2fveq3 6895	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → (dist‘(𝑅‘𝑦)) = (dist‘(𝑅‘𝑥)))
71		2fveq3 6895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑥)))
72	71, 10	eqtr4di 2788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = 𝑉)
73	72	sqxpeqd 5707	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))) = (𝑉 × 𝑉))
74	70, 73	reseq12d 5981	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)))
75	74, 11	eqtr4di 2788	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = 𝐸)
76	75	fveq2d 6894	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))))) = (ball‘𝐸))
77		fveq2 6890	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (𝑎‘𝑦) = (𝑎‘𝑥))
78		eqidd 2731	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → 𝑟 = 𝑟)
79	76, 77, 78	oveq123d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟) = ((𝑎‘𝑥)(ball‘𝐸)𝑟))
80	69, 79	oveq12d 7429	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
81	80	cbvmptv 5260	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
82	68, 81	fnmpti 6692	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼
83	82	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼)
84	16	adantlr 711	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉))
85		metxmet 24060	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉))
86	84, 85	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
87	15	ralrimiva 3144	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V)
88	87	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V)
89		simprl 767	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ 𝐵)
90	29	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝐵 = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
91	89, 90	eleqtrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
92	8, 9, 66, 67, 88, 10, 91	prdsbascl 17433	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 (𝑎‘𝑥) ∈ 𝑉)
93	92	r19.21bi 3246	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝑎‘𝑥) ∈ 𝑉)
94		simplrr 774	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ⁺)
95	94	rpred 13020	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ)
96		blbnd 36958	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
97	86, 93, 95, 96	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
98		ovex 7444	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V
99		xpeq12 5700	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∧ 𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
100	99	anidms 565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
101	100	reseq2d 5980	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝐸 ↾ (𝑦 × 𝑦)) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
102		fveq2 6890	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (TotBnd‘𝑦) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
103	101, 102	eleq12d 2825	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
104		fveq2 6890	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (Bnd‘𝑦) = (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
105	101, 104	eleq12d 2825	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
106	103, 105	bibi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦)) ↔ ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
107	106	imbi2d 339	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦))) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))))
108		prdsbnd2.m	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦)))
109	98, 107, 108	vtocl 3544	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
110	109	adantlr 711	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
111	97, 110	mpbird 256	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
112		eqid 2730	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))
113	80, 112, 68	fvmpt 6997	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐼 → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
114	113	adantl 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
115	114	fveq2d 6894	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
116		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))
117		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ (dist‘(𝑅‘𝑥)) = (dist‘(𝑅‘𝑥))
118	116, 117	ressds 17359	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V → (dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
119	98, 118	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
120	115, 119	eqtr4di 2788	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘(𝑅‘𝑥)))
121	114	fveq2d 6894	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
122		rpxr 12987	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
123	122	ad2antll 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑟 ∈ ℝ^*)
124	123	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ^*)
125		blssm 24144	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉)
126	86, 93, 124, 125	syl3anc 1369	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉)
127	116, 10	ressbas2 17186	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
128	126, 127	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
129	121, 128	eqtr4d 2773	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = ((𝑎‘𝑥)(ball‘𝐸)𝑟))
130	129	sqxpeqd 5707	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
131	120, 130	reseq12d 5981	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
132	11	reseq1i 5976	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
133		xpss12 5690	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 ∧ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉))
134	126, 126, 133	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉))
135	134	resabs1d 6011	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
136	132, 135	eqtrid 2782	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
137	131, 136	eqtr4d 2773	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
138	129	fveq2d 6894	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (TotBnd‘(Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
139	111, 137, 138	3eltr4d 2846	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((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	61, 62, 63, 64, 65, 66, 67, 83, 139	prdstotbnd 36965	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) ∈ (TotBnd‘(Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))))
141	24	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑌 = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
142		eqidd 2731	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
143		eqid 2730	. . . . . . . . . . . . 13 ⊢ (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
144	81	oveq2i 7422	. . . . . . . . . . . . . 14 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
145	144	fveq2i 6893	. . . . . . . . . . . . 13 ⊢ (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
146		fvexd 6905	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V)
147	98	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V)
148	141, 142, 143, 18, 145, 66, 66, 67, 146, 147	ressprdsds 24097	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))))))
149	128	ixpeq2dva 8908	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
150	69	cbvmptv 5260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)) = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))
151	150	oveq2i 7422	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
152	24, 151	eqtr4di 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑌 = (𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
153	152	fveq2d 6894	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
154	18, 153	eqtrid 2782	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
155	154	fveq2d 6894	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ball‘𝐷) = (ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))))
156	155	oveqdr 7439	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑎(ball‘𝐷)𝑟) = (𝑎(ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟))
157		eqid 2730	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
158		eqid 2730	. . . . . . . . . . . . . . . . 17 ⊢ (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
159	152	fveq2d 6894	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
160	27, 159	eqtrid 2782	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
161	160	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝐵 = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
162	89, 161	eleqtrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
163		rpgt0 12990	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 ∈ ℝ⁺ → 0 < 𝑟)
164	163	ad2antll 725	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 0 < 𝑟)
165	151, 157, 10, 11, 158, 66, 67, 146, 86, 162, 123, 164	prdsbl 24220	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑎(ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟))
166	156, 165	eqtrd 2770	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑎(ball‘𝐷)𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟))
167		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
168	68	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V)
169	168	ralrimiva 3144	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V)
170		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
171	167, 143, 66, 67, 169, 170	prdsbas3 17431	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
172	149, 166, 171	3eqtr4rd 2781	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (𝑎(ball‘𝐷)𝑟))
173	172	sqxpeqd 5707	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))) = ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
174	173	reseq2d 5980	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝐷 ↾ ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))))
175	148, 174	eqtrd 2770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))))
176	144	fveq2i 6893	. . . . . . . . . . . . 13 ⊢ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
177	176, 172	eqtrid 2782	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝑎(ball‘𝐷)𝑟))
178	177	fveq2d 6894	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (TotBnd‘(Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))) = (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
179	140, 175, 178	3eltr3d 2845	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
180	47, 48, 60, 179	syl12anc 833	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
181		totbndss 36948	. . . . . . . . 9 ⊢ (((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴))
182	180, 42, 181	syl2anc 582	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴))
183	46, 182	eqeltrrd 2832	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐶 ∈ (TotBnd‘𝐴))
184	41, 183	rexlimddv 3159	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (TotBnd‘𝐴))
185	184	exp32 419	. . . . 5 ⊢ (𝜑 → (𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
186	185	exlimdv 1934	. . . 4 ⊢ (𝜑 → (∃𝑎 𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
187	6, 186	biimtrid 241	. . 3 ⊢ (𝜑 → (𝐴 ≠ ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
188	5, 187	pm2.61dne 3026	. 2 ⊢ (𝜑 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))
189	1, 188	impbid2 225	1 ⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Bnd‘𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1539 ∃wex 1779 ∈ wcel 2104 ≠ wne 2938 ∀wral 3059 ∃wrex 3068 Vcvv 3472 ⊆ wss 3947 ∅c0 4321 class class class wbr 5147 ↦ cmpt 5230 × cxp 5673 ↾ cres 5677 Fn wfn 6537 ‘cfv 6542 (class class class)co 7411 Xcixp 8893 Fincfn 8941 ℝcr 11111 0cc0 11112 ℝ^*cxr 11251 < clt 11252 ℝ⁺crp 12978 Basecbs 17148 ↾_s cress 17177 distcds 17210 X_scprds 17395 ∞Metcxmet 21129 Metcmet 21130 ballcbl 21131 TotBndctotbnd 36937 Bndcbnd 36938

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-er 8705 df-ec 8707 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-sup 9439 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-z 12563 df-dec 12682 df-uz 12827 df-rp 12979 df-xneg 13096 df-xadd 13097 df-xmul 13098 df-icc 13335 df-fz 13489 df-struct 17084 df-sets 17101 df-slot 17119 df-ndx 17131 df-base 17149 df-ress 17178 df-plusg 17214 df-mulr 17215 df-sca 17217 df-vsca 17218 df-ip 17219 df-tset 17220 df-ple 17221 df-ds 17223 df-hom 17225 df-cco 17226 df-prds 17397 df-psmet 21136 df-xmet 21137 df-met 21138 df-bl 21139 df-totbnd 36939 df-bnd 36950

This theorem is referenced by: cnpwstotbnd 36968

W3C validator