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 35075

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 35069	. 2 ⊢ (𝐶 ∈ (TotBnd‘𝐴) → 𝐶 ∈ (Bnd‘𝐴))
2		bndmet 35061	. . . . 5 ⊢ (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (Met‘𝐴))
3		0totbnd 35053	. . . . 5 ⊢ (𝐴 = ∅ → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Met‘𝐴)))
4	2, 3	syl5ibr 248	. . . 4 ⊢ (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))
5	4	a1i 11	. . 3 ⊢ (𝜑 → (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
6		n0 4312	. . . 4 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑎 𝑎 ∈ 𝐴)
7		simprr 771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (Bnd‘𝐴))
8		eqid 2823	. . . . . . . . . . . 12 ⊢ (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
9		eqid 2823	. . . . . . . . . . . 12 ⊢ (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
10		prdsbnd.v	. . . . . . . . . . . 12 ⊢ 𝑉 = (Base‘(𝑅‘𝑥))
11		prdsbnd.e	. . . . . . . . . . . 12 ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉))
12		eqid 2823	. . . . . . . . . . . 12 ⊢ (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
13		prdsbnd.s	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ 𝑊)
14		prdsbnd.i	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ Fin)
15		fvexd 6687	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V)
16		prdsbnd2.e	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉))
17	8, 9, 10, 11, 12, 13, 14, 15, 16	prdsmet 22982	. . . . . . . . . . 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 6726	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 Fn 𝐼 ↔ 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
22	20, 21	sylib 220	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
23	22	oveq2d 7174	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆X_s𝑅) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
24	19, 23	syl5eq 2870	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
25	24	fveq2d 6676	. . . . . . . . . . . 12 ⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
26	18, 25	syl5eq 2870	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
27		prdsbnd.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝑌)
28	24	fveq2d 6676	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
29	27, 28	syl5eq 2870	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
30	29	fveq2d 6676	. . . . . . . . . . 11 ⊢ (𝜑 → (Met‘𝐵) = (Met‘(Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))))
31	17, 26, 30	3eltr4d 2930	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵))
32	31	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐷 ∈ (Met‘𝐵))
33		simpr 487	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐶 ∈ (Bnd‘𝐴))
34		prdsbnd2.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (𝐷 ↾ (𝐴 × 𝐴))
35	34	bnd2lem 35071	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐴 ⊆ 𝐵)
36	31, 33, 35	syl2an 597	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐴 ⊆ 𝐵)
37		simprl 769	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐴)
38	36, 37	sseldd 3970	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐵)
39	34	ssbnd 35068	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝑎 ∈ 𝐵) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)))
40	32, 38, 39	syl2anc 586	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)))
41	7, 40	mpbid 234	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))
42		simprr 771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))
43		xpss12 5572	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ (𝑎(ball‘𝐷)𝑟) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
44	42, 42, 43	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
45	44	resabs1d 5886	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = (𝐷 ↾ (𝐴 × 𝐴)))
46	45, 34	syl6eqr 2876	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = 𝐶)
47		simpll 765	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝜑)
48	38	adantr 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐵)
49		simprl 769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ)
50	37	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐴)
51	42, 50	sseldd 3970	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ (𝑎(ball‘𝐷)𝑟))
52	51	ne0d 4303	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝑎(ball‘𝐷)𝑟) ≠ ∅)
53	31	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (Met‘𝐵))
54		metxmet 22946	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵))
55	53, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (∞Met‘𝐵))
56	49	rexrd 10693	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ^*)
57		xbln0 23026	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^*) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
58	55, 48, 56, 57	syl3anc 1367	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
59	52, 58	mpbid 234	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 0 < 𝑟)
60	49, 59	elrpd 12431	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ⁺)
61		eqid 2823	. . . . . . . . . . . 12 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))
62		eqid 2823	. . . . . . . . . . . 12 ⊢ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))
63		eqid 2823	. . . . . . . . . . . 12 ⊢ (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))
64		eqid 2823	. . . . . . . . . . . 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 2823	. . . . . . . . . . . 12 ⊢ (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))
66	13	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑆 ∈ 𝑊)
67	14	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝐼 ∈ Fin)
68		ovex 7191	. . . . . . . . . . . . . 14 ⊢ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V
69		fveq2 6672	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥))
70		2fveq3 6677	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → (dist‘(𝑅‘𝑦)) = (dist‘(𝑅‘𝑥)))
71		2fveq3 6677	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑥)))
72	71, 10	syl6eqr 2876	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = 𝑉)
73	72	sqxpeqd 5589	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))) = (𝑉 × 𝑉))
74	70, 73	reseq12d 5856	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)))
75	74, 11	syl6eqr 2876	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = 𝐸)
76	75	fveq2d 6676	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))))) = (ball‘𝐸))
77		fveq2 6672	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (𝑎‘𝑦) = (𝑎‘𝑥))
78		eqidd 2824	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → 𝑟 = 𝑟)
79	76, 77, 78	oveq123d 7179	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟) = ((𝑎‘𝑥)(ball‘𝐸)𝑟))
80	69, 79	oveq12d 7176	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
81	80	cbvmptv 5171	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
82	68, 81	fnmpti 6493	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼
83	82	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼)
84	16	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉))
85		metxmet 22946	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉))
86	84, 85	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
87	15	ralrimiva 3184	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V)
88	87	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V)
89		simprl 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ 𝐵)
90	29	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝐵 = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
91	89, 90	eleqtrd 2917	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
92	8, 9, 66, 67, 88, 10, 91	prdsbascl 16758	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 (𝑎‘𝑥) ∈ 𝑉)
93	92	r19.21bi 3210	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝑎‘𝑥) ∈ 𝑉)
94		simplrr 776	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ⁺)
95	94	rpred 12434	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ)
96		blbnd 35067	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
97	86, 93, 95, 96	syl3anc 1367	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
98		ovex 7191	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V
99		xpeq12 5582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∧ 𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
100	99	anidms 569	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
101	100	reseq2d 5855	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝐸 ↾ (𝑦 × 𝑦)) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
102		fveq2 6672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (TotBnd‘𝑦) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
103	101, 102	eleq12d 2909	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
104		fveq2 6672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (Bnd‘𝑦) = (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
105	101, 104	eleq12d 2909	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
106	103, 105	bibi12d 348	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦)) ↔ ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
107	106	imbi2d 343	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦))) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))))
108		prdsbnd2.m	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦)))
109	98, 107, 108	vtocl 3561	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
110	109	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
111	97, 110	mpbird 259	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
112		eqid 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))
113	80, 112, 68	fvmpt 6770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐼 → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
114	113	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
115	114	fveq2d 6676	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
116		eqid 2823	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))
117		eqid 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (dist‘(𝑅‘𝑥)) = (dist‘(𝑅‘𝑥))
118	116, 117	ressds 16688	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V → (dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
119	98, 118	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
120	115, 119	syl6eqr 2876	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘(𝑅‘𝑥)))
121	114	fveq2d 6676	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
122		rpxr 12401	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
123	122	ad2antll 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑟 ∈ ℝ^*)
124	123	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ^*)
125		blssm 23030	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉)
126	86, 93, 124, 125	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉)
127	116, 10	ressbas2 16557	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
128	126, 127	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
129	121, 128	eqtr4d 2861	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = ((𝑎‘𝑥)(ball‘𝐸)𝑟))
130	129	sqxpeqd 5589	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
131	120, 130	reseq12d 5856	. . . . . . . . . . . . . 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 5851	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
133		xpss12 5572	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 ∧ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉))
134	126, 126, 133	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉))
135	134	resabs1d 5886	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
136	132, 135	syl5eq 2870	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
137	131, 136	eqtr4d 2861	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
138	129	fveq2d 6676	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (TotBnd‘(Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
139	111, 137, 138	3eltr4d 2930	. . . . . . . . . . . 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 35074	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) ∈ (TotBnd‘(Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))))
141	24	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑌 = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
142		eqidd 2824	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
143		eqid 2823	. . . . . . . . . . . . 13 ⊢ (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
144	81	oveq2i 7169	. . . . . . . . . . . . . 14 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
145	144	fveq2i 6675	. . . . . . . . . . . . 13 ⊢ (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
146		fvexd 6687	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V)
147	98	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V)
148	141, 142, 143, 18, 145, 66, 66, 67, 146, 147	ressprdsds 22983	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))))))
149	128	ixpeq2dva 8478	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
150	69	cbvmptv 5171	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)) = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))
151	150	oveq2i 7169	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
152	24, 151	syl6eqr 2876	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑌 = (𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
153	152	fveq2d 6676	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
154	18, 153	syl5eq 2870	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
155	154	fveq2d 6676	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ball‘𝐷) = (ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))))
156	155	oveqdr 7186	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑎(ball‘𝐷)𝑟) = (𝑎(ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟))
157		eqid 2823	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
158		eqid 2823	. . . . . . . . . . . . . . . . 17 ⊢ (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
159	152	fveq2d 6676	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
160	27, 159	syl5eq 2870	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
161	160	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝐵 = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
162	89, 161	eleqtrd 2917	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
163		rpgt0 12404	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 ∈ ℝ⁺ → 0 < 𝑟)
164	163	ad2antll 727	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 0 < 𝑟)
165	151, 157, 10, 11, 158, 66, 67, 146, 86, 162, 123, 164	prdsbl 23103	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑎(ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟))
166	156, 165	eqtrd 2858	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑎(ball‘𝐷)𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟))
167		eqid 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
168	68	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V)
169	168	ralrimiva 3184	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V)
170		eqid 2823	. . . . . . . . . . . . . . . 16 ⊢ (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
171	167, 143, 66, 67, 169, 170	prdsbas3 16756	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
172	149, 166, 171	3eqtr4rd 2869	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (𝑎(ball‘𝐷)𝑟))
173	172	sqxpeqd 5589	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))) = ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
174	173	reseq2d 5855	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝐷 ↾ ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))))
175	148, 174	eqtrd 2858	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))))
176	144	fveq2i 6675	. . . . . . . . . . . . 13 ⊢ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
177	176, 172	syl5eq 2870	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝑎(ball‘𝐷)𝑟))
178	177	fveq2d 6676	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (TotBnd‘(Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))) = (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
179	140, 175, 178	3eltr3d 2929	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
180	47, 48, 60, 179	syl12anc 834	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
181		totbndss 35057	. . . . . . . . 9 ⊢ (((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴))
182	180, 42, 181	syl2anc 586	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴))
183	46, 182	eqeltrrd 2916	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐶 ∈ (TotBnd‘𝐴))
184	41, 183	rexlimddv 3293	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (TotBnd‘𝐴))
185	184	exp32 423	. . . . 5 ⊢ (𝜑 → (𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
186	185	exlimdv 1934	. . . 4 ⊢ (𝜑 → (∃𝑎 𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
187	6, 186	syl5bi 244	. . 3 ⊢ (𝜑 → (𝐴 ≠ ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
188	5, 187	pm2.61dne 3105	. 2 ⊢ (𝜑 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))
189	1, 188	impbid2 228	1 ⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Bnd‘𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∃wex 1780 ∈ wcel 2114 ≠ wne 3018 ∀wral 3140 ∃wrex 3141 Vcvv 3496 ⊆ wss 3938 ∅c0 4293 class class class wbr 5068 ↦ cmpt 5148 × cxp 5555 ↾ cres 5559 Fn wfn 6352 ‘cfv 6357 (class class class)co 7158 Xcixp 8463 Fincfn 8511 ℝcr 10538 0cc0 10539 ℝ^*cxr 10676 < clt 10677 ℝ⁺crp 12392 Basecbs 16485 ↾_s cress 16486 distcds 16576 X_scprds 16721 ∞Metcxmet 20532 Metcmet 20533 ballcbl 20534 TotBndctotbnd 35046 Bndcbnd 35047

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616 ax-pre-sup 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-om 7583 df-1st 7691 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-2o 8105 df-oadd 8108 df-er 8291 df-ec 8293 df-map 8410 df-pm 8411 df-ixp 8464 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-sup 8908 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-div 11300 df-nn 11641 df-2 11703 df-3 11704 df-4 11705 df-5 11706 df-6 11707 df-7 11708 df-8 11709 df-9 11710 df-n0 11901 df-z 11985 df-dec 12102 df-uz 12247 df-rp 12393 df-xneg 12510 df-xadd 12511 df-xmul 12512 df-icc 12748 df-fz 12896 df-struct 16487 df-ndx 16488 df-slot 16489 df-base 16491 df-sets 16492 df-ress 16493 df-plusg 16580 df-mulr 16581 df-sca 16583 df-vsca 16584 df-ip 16585 df-tset 16586 df-ple 16587 df-ds 16589 df-hom 16591 df-cco 16592 df-prds 16723 df-psmet 20539 df-xmet 20540 df-met 20541 df-bl 20542 df-totbnd 35048 df-bnd 35059

This theorem is referenced by: cnpwstotbnd 35077

W3C validator