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 37761

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 37755	. 2 ⊢ (𝐶 ∈ (TotBnd‘𝐴) → 𝐶 ∈ (Bnd‘𝐴))
2		bndmet 37747	. . . . 5 ⊢ (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (Met‘𝐴))
3		0totbnd 37739	. . . . 5 ⊢ (𝐴 = ∅ → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Met‘𝐴)))
4	2, 3	imbitrrid 246	. . . 4 ⊢ (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))
5	4	a1i 11	. . 3 ⊢ (𝜑 → (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
6		n0 4333	. . . 4 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑎 𝑎 ∈ 𝐴)
7		simprr 772	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (Bnd‘𝐴))
8		eqid 2734	. . . . . . . . . . . 12 ⊢ (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
9		eqid 2734	. . . . . . . . . . . 12 ⊢ (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
10		prdsbnd.v	. . . . . . . . . . . 12 ⊢ 𝑉 = (Base‘(𝑅‘𝑥))
11		prdsbnd.e	. . . . . . . . . . . 12 ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉))
12		eqid 2734	. . . . . . . . . . . 12 ⊢ (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
13		prdsbnd.s	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ 𝑊)
14		prdsbnd.i	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ Fin)
15		fvexd 6901	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V)
16		prdsbnd2.e	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉))
17	8, 9, 10, 11, 12, 13, 14, 15, 16	prdsmet 24325	. . . . . . . . . . 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 6947	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 Fn 𝐼 ↔ 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
22	20, 21	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
23	22	oveq2d 7429	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆X_s𝑅) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
24	19, 23	eqtrid 2781	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
25	24	fveq2d 6890	. . . . . . . . . . . 12 ⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
26	18, 25	eqtrid 2781	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
27		prdsbnd.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝑌)
28	24	fveq2d 6890	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
29	27, 28	eqtrid 2781	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
30	29	fveq2d 6890	. . . . . . . . . . 11 ⊢ (𝜑 → (Met‘𝐵) = (Met‘(Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))))
31	17, 26, 30	3eltr4d 2848	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵))
32	31	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐷 ∈ (Met‘𝐵))
33		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐶 ∈ (Bnd‘𝐴))
34		prdsbnd2.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (𝐷 ↾ (𝐴 × 𝐴))
35	34	bnd2lem 37757	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐴 ⊆ 𝐵)
36	31, 33, 35	syl2an 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐴 ⊆ 𝐵)
37		simprl 770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐴)
38	36, 37	sseldd 3964	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐵)
39	34	ssbnd 37754	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝑎 ∈ 𝐵) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)))
40	32, 38, 39	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)))
41	7, 40	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))
42		simprr 772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))
43		xpss12 5680	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ (𝑎(ball‘𝐷)𝑟) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
44	42, 42, 43	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
45	44	resabs1d 6006	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = (𝐷 ↾ (𝐴 × 𝐴)))
46	45, 34	eqtr4di 2787	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = 𝐶)
47		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝜑)
48	38	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐵)
49		simprl 770	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ)
50	37	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ 𝐴)
51	42, 50	sseldd 3964	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ (𝑎(ball‘𝐷)𝑟))
52	51	ne0d 4322	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝑎(ball‘𝐷)𝑟) ≠ ∅)
53	31	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (Met‘𝐵))
54		metxmet 24289	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵))
55	53, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (∞Met‘𝐵))
56	49	rexrd 11293	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ^*)
57		xbln0 24369	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^*) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
58	55, 48, 56, 57	syl3anc 1372	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
59	52, 58	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 0 < 𝑟)
60	49, 59	elrpd 13056	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ⁺)
61		eqid 2734	. . . . . . . . . . . 12 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))
62		eqid 2734	. . . . . . . . . . . 12 ⊢ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))
63		eqid 2734	. . . . . . . . . . . 12 ⊢ (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))
64		eqid 2734	. . . . . . . . . . . 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 2734	. . . . . . . . . . . 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 7446	. . . . . . . . . . . . . 14 ⊢ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V
69		fveq2 6886	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥))
70		2fveq3 6891	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → (dist‘(𝑅‘𝑦)) = (dist‘(𝑅‘𝑥)))
71		2fveq3 6891	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑥)))
72	71, 10	eqtr4di 2787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = 𝑉)
73	72	sqxpeqd 5697	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))) = (𝑉 × 𝑉))
74	70, 73	reseq12d 5978	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)))
75	74, 11	eqtr4di 2787	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = 𝐸)
76	75	fveq2d 6890	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))))) = (ball‘𝐸))
77		fveq2 6886	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (𝑎‘𝑦) = (𝑎‘𝑥))
78		eqidd 2735	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → 𝑟 = 𝑟)
79	76, 77, 78	oveq123d 7434	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟) = ((𝑎‘𝑥)(ball‘𝐸)𝑟))
80	69, 79	oveq12d 7431	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
81	80	cbvmptv 5235	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
82	68, 81	fnmpti 6691	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼
83	82	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) Fn 𝐼)
84	16	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉))
85		metxmet 24289	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉))
86	84, 85	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
87	15	ralrimiva 3133	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V)
88	87	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V)
89		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ 𝐵)
90	29	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝐵 = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
91	89, 90	eleqtrd 2835	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
92	8, 9, 66, 67, 88, 10, 91	prdsbascl 17499	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 (𝑎‘𝑥) ∈ 𝑉)
93	92	r19.21bi 3237	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝑎‘𝑥) ∈ 𝑉)
94		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ⁺)
95	94	rpred 13059	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ)
96		blbnd 37753	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
97	86, 93, 95, 96	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
98		ovex 7446	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V
99		xpeq12 5690	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∧ 𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
100	99	anidms 566	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
101	100	reseq2d 5977	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝐸 ↾ (𝑦 × 𝑦)) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
102		fveq2 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (TotBnd‘𝑦) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
103	101, 102	eleq12d 2827	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
104		fveq2 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (Bnd‘𝑦) = (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
105	101, 104	eleq12d 2827	. . . . . . . . . . . . . . . . . 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 3541	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
110	109	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
111	97, 110	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
112		eqid 2734	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))
113	80, 112, 68	fvmpt 6996	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐼 → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
114	113	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
115	114	fveq2d 6890	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
116		eqid 2734	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))
117		eqid 2734	. . . . . . . . . . . . . . . . . 18 ⊢ (dist‘(𝑅‘𝑥)) = (dist‘(𝑅‘𝑥))
118	116, 117	ressds 17426	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V → (dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
119	98, 118	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
120	115, 119	eqtr4di 2787	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘(𝑅‘𝑥)))
121	114	fveq2d 6890	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
122		rpxr 13026	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
123	122	ad2antll 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑟 ∈ ℝ^*)
124	123	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ^*)
125		blssm 24373	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉)
126	86, 93, 124, 125	syl3anc 1372	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉)
127	116, 10	ressbas2 17261	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
128	126, 127	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
129	121, 128	eqtr4d 2772	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = ((𝑎‘𝑥)(ball‘𝐸)𝑟))
130	129	sqxpeqd 5697	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
131	120, 130	reseq12d 5978	. . . . . . . . . . . . . 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 5973	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
133		xpss12 5680	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 ∧ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉))
134	126, 126, 133	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉))
135	134	resabs1d 6006	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
136	132, 135	eqtrid 2781	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
137	131, 136	eqtr4d 2772	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
138	129	fveq2d 6890	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (TotBnd‘(Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
139	111, 137, 138	3eltr4d 2848	. . . . . . . . . . . 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 37760	. . . . . . . . . . 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 2735	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
143		eqid 2734	. . . . . . . . . . . . 13 ⊢ (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
144	81	oveq2i 7424	. . . . . . . . . . . . . 14 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
145	144	fveq2i 6889	. . . . . . . . . . . . 13 ⊢ (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
146		fvexd 6901	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V)
147	98	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V)
148	141, 142, 143, 18, 145, 66, 66, 67, 146, 147	ressprdsds 24326	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))))))
149	128	ixpeq2dva 8934	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
150	69	cbvmptv 5235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)) = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))
151	150	oveq2i 7424	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
152	24, 151	eqtr4di 2787	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑌 = (𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
153	152	fveq2d 6890	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
154	18, 153	eqtrid 2781	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
155	154	fveq2d 6890	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ball‘𝐷) = (ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))))
156	155	oveqdr 7441	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑎(ball‘𝐷)𝑟) = (𝑎(ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟))
157		eqid 2734	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
158		eqid 2734	. . . . . . . . . . . . . . . . 17 ⊢ (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
159	152	fveq2d 6890	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
160	27, 159	eqtrid 2781	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
161	160	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝐵 = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
162	89, 161	eleqtrd 2835	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
163		rpgt0 13029	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 ∈ ℝ⁺ → 0 < 𝑟)
164	163	ad2antll 729	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 0 < 𝑟)
165	151, 157, 10, 11, 158, 66, 67, 146, 86, 162, 123, 164	prdsbl 24448	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑎(ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟))
166	156, 165	eqtrd 2769	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑎(ball‘𝐷)𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟))
167		eqid 2734	. . . . . . . . . . . . . . . 16 ⊢ (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
168	68	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V)
169	168	ralrimiva 3133	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V)
170		eqid 2734	. . . . . . . . . . . . . . . 16 ⊢ (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
171	167, 143, 66, 67, 169, 170	prdsbas3 17497	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
172	149, 166, 171	3eqtr4rd 2780	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (𝑎(ball‘𝐷)𝑟))
173	172	sqxpeqd 5697	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))) = ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
174	173	reseq2d 5977	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝐷 ↾ ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))))
175	148, 174	eqtrd 2769	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))))
176	144	fveq2i 6889	. . . . . . . . . . . . 13 ⊢ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
177	176, 172	eqtrid 2781	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝑎(ball‘𝐷)𝑟))
178	177	fveq2d 6890	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (TotBnd‘(Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))) = (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
179	140, 175, 178	3eltr3d 2847	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
180	47, 48, 60, 179	syl12anc 836	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
181		totbndss 37743	. . . . . . . . 9 ⊢ (((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴))
182	180, 42, 181	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) ∈ (TotBnd‘𝐴))
183	46, 182	eqeltrrd 2834	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐶 ∈ (TotBnd‘𝐴))
184	41, 183	rexlimddv 3148	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (TotBnd‘𝐴))
185	184	exp32 420	. . . . 5 ⊢ (𝜑 → (𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
186	185	exlimdv 1932	. . . 4 ⊢ (𝜑 → (∃𝑎 𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
187	6, 186	biimtrid 242	. . 3 ⊢ (𝜑 → (𝐴 ≠ ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
188	5, 187	pm2.61dne 3017	. 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 1539 ∃wex 1778 ∈ wcel 2107 ≠ wne 2931 ∀wral 3050 ∃wrex 3059 Vcvv 3463 ⊆ wss 3931 ∅c0 4313 class class class wbr 5123 ↦ cmpt 5205 × cxp 5663 ↾ cres 5667 Fn wfn 6536 ‘cfv 6541 (class class class)co 7413 Xcixp 8919 Fincfn 8967 ℝcr 11136 0cc0 11137 ℝ^*cxr 11276 < clt 11277 ℝ⁺crp 13016 Basecbs 17229 ↾_s cress 17252 distcds 17282 X_scprds 17461 ∞Metcxmet 21311 Metcmet 21312 ballcbl 21313 TotBndctotbnd 37732 Bndcbnd 37733

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-cnex 11193 ax-resscn 11194 ax-1cn 11195 ax-icn 11196 ax-addcl 11197 ax-addrcl 11198 ax-mulcl 11199 ax-mulrcl 11200 ax-mulcom 11201 ax-addass 11202 ax-mulass 11203 ax-distr 11204 ax-i2m1 11205 ax-1ne0 11206 ax-1rid 11207 ax-rnegex 11208 ax-rrecex 11209 ax-cnre 11210 ax-pre-lttri 11211 ax-pre-lttrn 11212 ax-pre-ltadd 11213 ax-pre-mulgt0 11214 ax-pre-sup 11215

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-iun 4973 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7870 df-1st 7996 df-2nd 7997 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-er 8727 df-ec 8729 df-map 8850 df-pm 8851 df-ixp 8920 df-en 8968 df-dom 8969 df-sdom 8970 df-fin 8971 df-sup 9464 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-sub 11476 df-neg 11477 df-div 11903 df-nn 12249 df-2 12311 df-3 12312 df-4 12313 df-5 12314 df-6 12315 df-7 12316 df-8 12317 df-9 12318 df-n0 12510 df-z 12597 df-dec 12717 df-uz 12861 df-rp 13017 df-xneg 13136 df-xadd 13137 df-xmul 13138 df-icc 13376 df-fz 13530 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17230 df-ress 17253 df-plusg 17286 df-mulr 17287 df-sca 17289 df-vsca 17290 df-ip 17291 df-tset 17292 df-ple 17293 df-ds 17295 df-hom 17297 df-cco 17298 df-prds 17463 df-psmet 21318 df-xmet 21319 df-met 21320 df-bl 21321 df-totbnd 37734 df-bnd 37745

This theorem is referenced by: cnpwstotbnd 37763

W3C validator