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 37781

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 37775	. 2 ⊢ (𝐶 ∈ (TotBnd‘𝐴) → 𝐶 ∈ (Bnd‘𝐴))
2		bndmet 37767	. . . . 5 ⊢ (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (Met‘𝐴))
3		0totbnd 37759	. . . . 5 ⊢ (𝐴 = ∅ → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Met‘𝐴)))
4	2, 3	imbitrrid 246	. . . 4 ⊢ (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴)))
5	4	a1i 11	. . 3 ⊢ (𝜑 → (𝐴 = ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
6		n0 4358	. . . 4 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑎 𝑎 ∈ 𝐴)
7		simprr 773	. . . . . . . 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 6921	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V)
16		prdsbnd2.e	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉))
17	8, 9, 10, 11, 12, 13, 14, 15, 16	prdsmet 24395	. . . . . . . . . . 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 6966	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 Fn 𝐼 ↔ 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
22	20, 21	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
23	22	oveq2d 7446	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆X_s𝑅) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
24	19, 23	eqtrid 2786	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
25	24	fveq2d 6910	. . . . . . . . . . . 12 ⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
26	18, 25	eqtrid 2786	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
27		prdsbnd.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝑌)
28	24	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
29	27, 28	eqtrid 2786	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
30	29	fveq2d 6910	. . . . . . . . . . 11 ⊢ (𝜑 → (Met‘𝐵) = (Met‘(Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))))
31	17, 26, 30	3eltr4d 2853	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵))
32	31	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐷 ∈ (Met‘𝐵))
33		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐶 ∈ (Bnd‘𝐴))
34		prdsbnd2.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (𝐷 ↾ (𝐴 × 𝐴))
35	34	bnd2lem 37777	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝐶 ∈ (Bnd‘𝐴)) → 𝐴 ⊆ 𝐵)
36	31, 33, 35	syl2an 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐴 ⊆ 𝐵)
37		simprl 771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐴)
38	36, 37	sseldd 3995	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝑎 ∈ 𝐵)
39	34	ssbnd 37774	. . . . . . . . 9 ⊢ ((𝐷 ∈ (Met‘𝐵) ∧ 𝑎 ∈ 𝐵) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)))
40	32, 38, 39	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → (𝐶 ∈ (Bnd‘𝐴) ↔ ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)))
41	7, 40	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → ∃𝑟 ∈ ℝ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))
42		simprr 773	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))
43		xpss12 5703	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ (𝑎(ball‘𝐷)𝑟) ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟)) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
44	42, 42, 43	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐴 × 𝐴) ⊆ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
45	44	resabs1d 6027	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ↾ (𝐴 × 𝐴)) = (𝐷 ↾ (𝐴 × 𝐴)))
46	45, 34	eqtr4di 2792	. . . . . . . 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 3995	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑎 ∈ (𝑎(ball‘𝐷)𝑟))
52	51	ne0d 4347	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝑎(ball‘𝐷)𝑟) ≠ ∅)
53	31	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (Met‘𝐵))
54		metxmet 24359	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵))
55	53, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐷 ∈ (∞Met‘𝐵))
56	49	rexrd 11308	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝑟 ∈ ℝ^*)
57		xbln0 24439	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ^*) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
58	55, 48, 56, 57	syl3anc 1370	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → ((𝑎(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟))
59	52, 58	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 0 < 𝑟)
60	49, 59	elrpd 13071	. . . . . . . . . 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 7463	. . . . . . . . . . . . . 14 ⊢ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V
69		fveq2 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥))
70		2fveq3 6911	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → (dist‘(𝑅‘𝑦)) = (dist‘(𝑅‘𝑥)))
71		2fveq3 6911	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑥)))
72	71, 10	eqtr4di 2792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → (Base‘(𝑅‘𝑦)) = 𝑉)
73	72	sqxpeqd 5720	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))) = (𝑉 × 𝑉))
74	70, 73	reseq12d 6000	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)))
75	74, 11	eqtr4di 2792	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))) = 𝐸)
76	75	fveq2d 6910	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦))))) = (ball‘𝐸))
77		fveq2 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (𝑎‘𝑦) = (𝑎‘𝑥))
78		eqidd 2735	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → 𝑟 = 𝑟)
79	76, 77, 78	oveq123d 7451	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟) = ((𝑎‘𝑥)(ball‘𝐸)𝑟))
80	69, 79	oveq12d 7448	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
81	80	cbvmptv 5260	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))) = (𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
82	68, 81	fnmpti 6711	. . . . . . . . . . . . 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 24359	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉))
86	84, 85	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
87	15	ralrimiva 3143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V)
88	87	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 (𝑅‘𝑥) ∈ V)
89		simprl 771	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ 𝐵)
90	29	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝐵 = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
91	89, 90	eleqtrd 2840	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
92	8, 9, 66, 67, 88, 10, 91	prdsbascl 17529	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 (𝑎‘𝑥) ∈ 𝑉)
93	92	r19.21bi 3248	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝑎‘𝑥) ∈ 𝑉)
94		simplrr 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ⁺)
95	94	rpred 13074	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ)
96		blbnd 37773	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
97	86, 93, 95, 96	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
98		ovex 7463	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V
99		xpeq12 5713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∧ 𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟)) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
100	99	anidms 566	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝑦 × 𝑦) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
101	100	reseq2d 5999	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (𝐸 ↾ (𝑦 × 𝑦)) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
102		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (TotBnd‘𝑦) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
103	101, 102	eleq12d 2832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) ∈ (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟))))
104		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑎‘𝑥)(ball‘𝐸)𝑟) → (Bnd‘𝑦) = (Bnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
105	101, 104	eleq12d 2832	. . . . . . . . . . . . . . . . . 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 3557	. . . . . . . . . . . . . . 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 7015	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐼 → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
114	113	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥) = ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
115	114	fveq2d 6910	. . . . . . . . . . . . . . . 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 17455	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V → (dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
119	98, 118	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (dist‘(𝑅‘𝑥)) = (dist‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
120	115, 119	eqtr4di 2792	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (dist‘(𝑅‘𝑥)))
121	114	fveq2d 6910	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
122		rpxr 13041	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
123	122	ad2antll 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑟 ∈ ℝ^*)
124	123	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ^*)
125		blssm 24443	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑎‘𝑥) ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉)
126	86, 93, 124, 125	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉)
127	116, 10	ressbas2 17282	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
128	126, 127	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
129	121, 128	eqtr4d 2777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) = ((𝑎‘𝑥)(ball‘𝐸)𝑟))
130	129	sqxpeqd 5720	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
131	120, 130	reseq12d 6000	. . . . . . . . . . . . . 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 5995	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
133		xpss12 5703	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉 ∧ ((𝑎‘𝑥)(ball‘𝐸)𝑟) ⊆ 𝑉) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉))
134	126, 126, 133	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ⊆ (𝑉 × 𝑉))
135	134	resabs1d 6027	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
136	132, 135	eqtrid 2786	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = ((dist‘(𝑅‘𝑥)) ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
137	131, 136	eqtr4d 2777	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((dist‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) ↾ ((Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)) × (Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥)))) = (𝐸 ↾ (((𝑎‘𝑥)(ball‘𝐸)𝑟) × ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
138	129	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (TotBnd‘(Base‘((𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))‘𝑥))) = (TotBnd‘((𝑎‘𝑥)(ball‘𝐸)𝑟)))
139	111, 137, 138	3eltr4d 2853	. . . . . . . . . . . 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 37780	. . . . . . . . . . 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 7441	. . . . . . . . . . . . . 14 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
145	144	fveq2i 6909	. . . . . . . . . . . . 13 ⊢ (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (dist‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
146		fvexd 6921	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V)
147	98	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) ∧ 𝑥 ∈ 𝐼) → ((𝑎‘𝑥)(ball‘𝐸)𝑟) ∈ V)
148	141, 142, 143, 18, 145, 66, 66, 67, 146, 147	ressprdsds 24396	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))))))
149	128	ixpeq2dva 8950	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
150	69	cbvmptv 5260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)) = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))
151	150	oveq2i 7441	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))) = (𝑆X_s(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
152	24, 151	eqtr4di 2792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑌 = (𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
153	152	fveq2d 6910	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
154	18, 153	eqtrid 2786	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 = (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
155	154	fveq2d 6910	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ball‘𝐷) = (ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))))
156	155	oveqdr 7458	. . . . . . . . . . . . . . . 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 6910	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
160	27, 159	eqtrid 2786	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
161	160	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝐵 = (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
162	89, 161	eleqtrd 2840	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 𝑎 ∈ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
163		rpgt0 13044	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 ∈ ℝ⁺ → 0 < 𝑟)
164	163	ad2antll 729	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → 0 < 𝑟)
165	151, 157, 10, 11, 158, 66, 67, 146, 86, 162, 123, 164	prdsbl 24519	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝑎(ball‘(dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟) = X𝑥 ∈ 𝐼 ((𝑎‘𝑥)(ball‘𝐸)𝑟))
166	156, 165	eqtrd 2774	. . . . . . . . . . . . . . 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 3143	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ∀𝑥 ∈ 𝐼 ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)) ∈ V)
170		eqid 2734	. . . . . . . . . . . . . . . 16 ⊢ (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))) = (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))
171	167, 143, 66, 67, 169, 170	prdsbas3 17527	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = X𝑥 ∈ 𝐼 (Base‘((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))
172	149, 166, 171	3eqtr4rd 2785	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) = (𝑎(ball‘𝐷)𝑟))
173	172	sqxpeqd 5720	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))) = ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟)))
174	173	reseq2d 5999	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝐷 ↾ ((Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))) × (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟))))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))))
175	148, 174	eqtrd 2774	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (dist‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))))
176	144	fveq2i 6909	. . . . . . . . . . . . 13 ⊢ (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (Base‘(𝑆X_s(𝑥 ∈ 𝐼 ↦ ((𝑅‘𝑥) ↾_s ((𝑎‘𝑥)(ball‘𝐸)𝑟)))))
177	176, 172	eqtrid 2786	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟))))) = (𝑎(ball‘𝐷)𝑟))
178	177	fveq2d 6910	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (TotBnd‘(Base‘(𝑆X_s(𝑦 ∈ 𝐼 ↦ ((𝑅‘𝑦) ↾_s ((𝑎‘𝑦)(ball‘((dist‘(𝑅‘𝑦)) ↾ ((Base‘(𝑅‘𝑦)) × (Base‘(𝑅‘𝑦)))))𝑟)))))) = (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
179	140, 175, 178	3eltr3d 2852	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑟 ∈ ℝ⁺)) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
180	47, 48, 60, 179	syl12anc 837	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → (𝐷 ↾ ((𝑎(ball‘𝐷)𝑟) × (𝑎(ball‘𝐷)𝑟))) ∈ (TotBnd‘(𝑎(ball‘𝐷)𝑟)))
181		totbndss 37763	. . . . . . . . 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 2839	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) ∧ (𝑟 ∈ ℝ ∧ 𝐴 ⊆ (𝑎(ball‘𝐷)𝑟))) → 𝐶 ∈ (TotBnd‘𝐴))
184	41, 183	rexlimddv 3158	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝐶 ∈ (Bnd‘𝐴))) → 𝐶 ∈ (TotBnd‘𝐴))
185	184	exp32 420	. . . . 5 ⊢ (𝜑 → (𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
186	185	exlimdv 1930	. . . 4 ⊢ (𝜑 → (∃𝑎 𝑎 ∈ 𝐴 → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
187	6, 186	biimtrid 242	. . 3 ⊢ (𝜑 → (𝐴 ≠ ∅ → (𝐶 ∈ (Bnd‘𝐴) → 𝐶 ∈ (TotBnd‘𝐴))))
188	5, 187	pm2.61dne 3025	. 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 1536 ∃wex 1775 ∈ wcel 2105 ≠ wne 2937 ∀wral 3058 ∃wrex 3067 Vcvv 3477 ⊆ wss 3962 ∅c0 4338 class class class wbr 5147 ↦ cmpt 5230 × cxp 5686 ↾ cres 5690 Fn wfn 6557 ‘cfv 6562 (class class class)co 7430 Xcixp 8935 Fincfn 8983 ℝcr 11151 0cc0 11152 ℝ^*cxr 11291 < clt 11292 ℝ⁺crp 13031 Basecbs 17244 ↾_s cress 17273 distcds 17306 X_scprds 17491 ∞Metcxmet 21366 Metcmet 21367 ballcbl 21368 TotBndctotbnd 37752 Bndcbnd 37753

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-rep 5284 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-cnex 11208 ax-resscn 11209 ax-1cn 11210 ax-icn 11211 ax-addcl 11212 ax-addrcl 11213 ax-mulcl 11214 ax-mulrcl 11215 ax-mulcom 11216 ax-addass 11217 ax-mulass 11218 ax-distr 11219 ax-i2m1 11220 ax-1ne0 11221 ax-1rid 11222 ax-rnegex 11223 ax-rrecex 11224 ax-cnre 11225 ax-pre-lttri 11226 ax-pre-lttrn 11227 ax-pre-ltadd 11228 ax-pre-mulgt0 11229 ax-pre-sup 11230

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-pss 3982 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-tp 4635 df-op 4637 df-uni 4912 df-iun 4997 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5640 df-we 5642 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-pred 6322 df-ord 6388 df-on 6389 df-lim 6390 df-suc 6391 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-om 7887 df-1st 8012 df-2nd 8013 df-frecs 8304 df-wrecs 8335 df-recs 8409 df-rdg 8448 df-1o 8504 df-er 8743 df-ec 8745 df-map 8866 df-pm 8867 df-ixp 8936 df-en 8984 df-dom 8985 df-sdom 8986 df-fin 8987 df-sup 9479 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11491 df-neg 11492 df-div 11918 df-nn 12264 df-2 12326 df-3 12327 df-4 12328 df-5 12329 df-6 12330 df-7 12331 df-8 12332 df-9 12333 df-n0 12524 df-z 12611 df-dec 12731 df-uz 12876 df-rp 13032 df-xneg 13151 df-xadd 13152 df-xmul 13153 df-icc 13390 df-fz 13544 df-struct 17180 df-sets 17197 df-slot 17215 df-ndx 17227 df-base 17245 df-ress 17274 df-plusg 17310 df-mulr 17311 df-sca 17313 df-vsca 17314 df-ip 17315 df-tset 17316 df-ple 17317 df-ds 17319 df-hom 17321 df-cco 17322 df-prds 17493 df-psmet 21373 df-xmet 21374 df-met 21375 df-bl 21376 df-totbnd 37754 df-bnd 37765

This theorem is referenced by: cnpwstotbnd 37783

W3C validator