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 38046

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 38040	. 2 ⊢ (𝐶 ∈ (TotBnd‘𝐴) → 𝐶 ∈ (Bnd‘𝐴))
2		bndmet 38032	. . . . 5 ⊢ (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (Met‘𝐴))
3		0totbnd 38024	. . . . 5 ⊢ (𝐴 = ∅ → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Met‘𝐴)))
4	2, 3	imbitrrid 246	. . . 4 ⊢ (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))
5	4	a1i 11	. . 3 ⊢ (𝜑 → (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
6		n0 4307	. . . 4 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑎 𝑎 ∈ 𝐴)
7		simprr 773	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (Bnd‘𝐴))
8		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
9		eqid 2737	. . . . . . . . . . . 12 ⊢ (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
10		prdsbnd.v	. . . . . . . . . . . 12 ⊢ 𝑉 = (Base‘(𝑅‘𝑥))
11		prdsbnd.e	. . . . . . . . . . . 12 ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉))
12		eqid 2737	. . . . . . . . . . . 12 ⊢ (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
13		prdsbnd.s	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ 𝑊)
14		prdsbnd.i	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ Fin)
15		fvexd 6857	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V)
16		prdsbnd2.e	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉))
17	8, 9, 10, 11, 12, 13, 14, 15, 16	prdsmet 24326	. . . . . . . . . . 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 6900	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 Fn 𝐼 ↔ 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
22	20, 21	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
23	22	oveq2d 7384	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆X_s𝑅) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
24	19, 23	eqtrid 2784	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
25	24	fveq2d 6846	. . . . . . . . . . . 12 ⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
26	18, 25	eqtrid 2784	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
27		prdsbnd.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝑌)
28	24	fveq2d 6846	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
29	27, 28	eqtrid 2784	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
30	29	fveq2d 6846	. . . . . . . . . . 11 ⊢ (𝜑 → (Met‘𝐵) = (Met‘(Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))))
31	17, 26, 30	3eltr4d 2852	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵))
32	31	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐷 ∈ (Met‘𝐵))
33		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐶 ∈ (Bnd‘𝐴))
34		prdsbnd2.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (𝐷 ↾ (𝐴 × 𝐴))
35	34	bnd2lem 38042	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐴 ⊆ 𝐵)
36	31, 33, 35	syl2an 597	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐴 ⊆ 𝐵)
37		simprl 771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐴)
38	36, 37	sseldd 3936	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐵)
39	34	ssbnd 38039	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝑎 ∈ 𝐵) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)))
40	32, 38, 39	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)))
41	7, 40	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))
42		simprr 773	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))
43		xpss12 5647	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ (𝑎(ball‘𝐷)𝑟) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
44	42, 42, 43	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
45	44	resabs1d 5975	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = (𝐷 ↾ (𝐴 × 𝐴)))
46	45, 34	eqtr4di 2790	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = 𝐶)
47		simpll 767	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝜑)
48	38	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐵)
49		simprl 771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ)
50	37	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐴)
51	42, 50	sseldd 3936	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ (𝑎(ball‘𝐷)𝑟))
52	51	ne0d 4296	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝑎(ball‘𝐷)𝑟) ≠ ∅)
53	31	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (Met‘𝐵))
54		metxmet 24290	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵))
55	53, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (∞Met‘𝐵))
56	49	rexrd 11194	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ^*)
57		xbln0 24370	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^*) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
58	55, 48, 56, 57	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
59	52, 58	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 0 < 𝑟)
60	49, 59	elrpd 12958	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ⁺)
61		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))
62		eqid 2737	. . . . . . . . . . . 12 ⊢ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))
63		eqid 2737	. . . . . . . . . . . 12 ⊢ (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))
64		eqid 2737	. . . . . . . . . . . 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 2737	. . . . . . . . . . . 12 ⊢ (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))
66	13	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑆 ∈ 𝑊)
67	14	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝐼 ∈ Fin)
68		ovex 7401	. . . . . . . . . . . . . 14 ⊢ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V
69		fveq2 6842	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥))
70		2fveq3 6847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → (dist‘(𝑅‘𝑦)) = (dist‘(𝑅‘𝑥)))
71		2fveq3 6847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑥)))
72	71, 10	eqtr4di 2790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = 𝑉)
73	72	sqxpeqd 5664	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))) = (𝑉 × 𝑉))
74	70, 73	reseq12d 5947	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)))
75	74, 11	eqtr4di 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = 𝐸)
76	75	fveq2d 6846	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))))) = (ball‘𝐸))
77		fveq2 6842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (𝑎‘𝑦) = (𝑎‘𝑥))
78		eqidd 2738	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → 𝑟 = 𝑟)
79	76, 77, 78	oveq123d 7389	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟) = ((𝑎‘𝑥)(ball‘𝐸)𝑟))
80	69, 79	oveq12d 7386	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
81	80	cbvmptv 5204	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
82	68, 81	fnmpti 6643	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼
83	82	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼)
84	16	adantlr 716	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉))
85		metxmet 24290	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉))
86	84, 85	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
87	15	ralrimiva 3130	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V)
88	87	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V)
89		simprl 771	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ 𝐵)
90	29	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝐵 = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
91	89, 90	eleqtrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
92	8, 9, 66, 67, 88, 10, 91	prdsbascl 17415	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 (𝑎‘𝑥) ∈ 𝑉)
93	92	r19.21bi 3230	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝑎‘𝑥) ∈ 𝑉)
94		simplrr 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ⁺)
95	94	rpred 12961	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ)
96		blbnd 38038	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
97	86, 93, 95, 96	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
98		ovex 7401	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V
99		xpeq12 5657	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∧ 𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
100	99	anidms 566	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
101	100	reseq2d 5946	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝐸 ↾ (𝑦 × 𝑦)) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
102		fveq2 6842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (TotBnd‘𝑦) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
103	101, 102	eleq12d 2831	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
104		fveq2 6842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (Bnd‘𝑦) = (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
105	101, 104	eleq12d 2831	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
106	103, 105	bibi12d 345	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦)) ↔ ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
107	106	imbi2d 340	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦))) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))))
108		prdsbnd2.m	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦)))
109	98, 107, 108	vtocl 3517	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
110	109	adantlr 716	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
111	97, 110	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
112		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))
113	80, 112, 68	fvmpt 6949	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐼 → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
114	113	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
115	114	fveq2d 6846	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
116		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))
117		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (dist‘(𝑅‘𝑥)) = (dist‘(𝑅‘𝑥))
118	116, 117	ressds 17342	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V → (dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
119	98, 118	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
120	115, 119	eqtr4di 2790	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘(𝑅‘𝑥)))
121	114	fveq2d 6846	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
122		rpxr 12927	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
123	122	ad2antll 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑟 ∈ ℝ^*)
124	123	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ^*)
125		blssm 24374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉)
126	86, 93, 124, 125	syl3anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉)
127	116, 10	ressbas2 17177	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
128	126, 127	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
129	121, 128	eqtr4d 2775	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = ((𝑎‘𝑥)(ball‘𝐸)𝑟))
130	129	sqxpeqd 5664	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
131	120, 130	reseq12d 5947	. . . . . . . . . . . . . 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 5942	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
133		xpss12 5647	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 ∧ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉))
134	126, 126, 133	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉))
135	134	resabs1d 5975	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
136	132, 135	eqtrid 2784	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
137	131, 136	eqtr4d 2775	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
138	129	fveq2d 6846	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (TotBnd‘(Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
139	111, 137, 138	3eltr4d 2852	. . . . . . . . . . . 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 38045	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) ∈ (TotBnd‘(Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))))
141	24	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑌 = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
142		eqidd 2738	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
143		eqid 2737	. . . . . . . . . . . . 13 ⊢ (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
144	81	oveq2i 7379	. . . . . . . . . . . . . 14 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
145	144	fveq2i 6845	. . . . . . . . . . . . 13 ⊢ (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
146		fvexd 6857	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V)
147	98	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V)
148	141, 142, 143, 18, 145, 66, 66, 67, 146, 147	ressprdsds 24327	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))))))
149	128	ixpeq2dva 8862	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
150	69	cbvmptv 5204	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)) = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))
151	150	oveq2i 7379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
152	24, 151	eqtr4di 2790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑌 = (𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
153	152	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
154	18, 153	eqtrid 2784	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
155	154	fveq2d 6846	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ball‘𝐷) = (ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))))
156	155	oveqdr 7396	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑎(ball‘𝐷)𝑟) = (𝑎(ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟))
157		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
158		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
159	152	fveq2d 6846	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
160	27, 159	eqtrid 2784	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
161	160	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝐵 = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
162	89, 161	eleqtrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
163		rpgt0 12930	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 ∈ ℝ⁺ → 0 < 𝑟)
164	163	ad2antll 730	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 0 < 𝑟)
165	151, 157, 10, 11, 158, 66, 67, 146, 86, 162, 123, 164	prdsbl 24447	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑎(ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟))
166	156, 165	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑎(ball‘𝐷)𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟))
167		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
168	68	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V)
169	168	ralrimiva 3130	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V)
170		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
171	167, 143, 66, 67, 169, 170	prdsbas3 17413	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
172	149, 166, 171	3eqtr4rd 2783	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (𝑎(ball‘𝐷)𝑟))
173	172	sqxpeqd 5664	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))) = ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
174	173	reseq2d 5946	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝐷 ↾ ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))))
175	148, 174	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))))
176	144	fveq2i 6845	. . . . . . . . . . . . 13 ⊢ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
177	176, 172	eqtrid 2784	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝑎(ball‘𝐷)𝑟))
178	177	fveq2d 6846	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (TotBnd‘(Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))) = (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
179	140, 175, 178	3eltr3d 2851	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
180	47, 48, 60, 179	syl12anc 837	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
181		totbndss 38028	. . . . . . . . 9 ⊢ (((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴))
182	180, 42, 181	syl2anc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴))
183	46, 182	eqeltrrd 2838	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐶 ∈ (TotBnd‘𝐴))
184	41, 183	rexlimddv 3145	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (TotBnd‘𝐴))
185	184	exp32 420	. . . . 5 ⊢ (𝜑 → (𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
186	185	exlimdv 1935	. . . 4 ⊢ (𝜑 → (∃𝑎 𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
187	6, 186	biimtrid 242	. . 3 ⊢ (𝜑 → (𝐴 ≠ ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
188	5, 187	pm2.61dne 3019	. 2 ⊢ (𝜑 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))
189	1, 188	impbid2 226	1 ⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Bnd‘𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 Vcvv 3442 ⊆ wss 3903 ∅c0 4287 class class class wbr 5100 ↦ cmpt 5181 × cxp 5630 ↾ cres 5634 Fn wfn 6495 ‘cfv 6500 (class class class)co 7368 Xcixp 8847 Fincfn 8895 ℝcr 11037 0cc0 11038 ℝ^*cxr 11177 < clt 11178 ℝ⁺crp 12917 Basecbs 17148 ↾_s cress 17169 distcds 17198 X_scprds 17377 ∞Metcxmet 21306 Metcmet 21307 ballcbl 21308 TotBndctotbnd 38017 Bndcbnd 38018

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-er 8645 df-ec 8647 df-map 8777 df-pm 8778 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9357 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-7 12225 df-8 12226 df-9 12227 df-n0 12414 df-z 12501 df-dec 12620 df-uz 12764 df-rp 12918 df-xneg 13038 df-xadd 13039 df-xmul 13040 df-icc 13280 df-fz 13436 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-sca 17205 df-vsca 17206 df-ip 17207 df-tset 17208 df-ple 17209 df-ds 17211 df-hom 17213 df-cco 17214 df-prds 17379 df-psmet 21313 df-xmet 21314 df-met 21315 df-bl 21316 df-totbnd 38019 df-bnd 38030

This theorem is referenced by: cnpwstotbnd 38048

W3C validator