Theorem prdstotbnd 33593

Description: The product metric over finite index set is totally bounded if all the factors are totally bounded. (Contributed by Mario Carneiro, 20-Sep-2015.)

Hypotheses

Ref	Expression
prdsbnd.y	⊢ 𝑌 = (𝑆Xs𝑅)
prdsbnd.b	⊢ 𝐵 = (Base‘𝑌)
prdsbnd.v	⊢ 𝑉 = (Base‘(𝑅‘𝑥))
prdsbnd.e	⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉))
prdsbnd.d	⊢ 𝐷 = (dist‘𝑌)
prdsbnd.s	⊢ (𝜑 → 𝑆 ∈ 𝑊)
prdsbnd.i	⊢ (𝜑 → 𝐼 ∈ Fin)
prdsbnd.r	⊢ (𝜑 → 𝑅 Fn 𝐼)
prdstotbnd.m	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (TotBnd‘𝑉))

Assertion

Ref	Expression
prdstotbnd	⊢ (𝜑 → 𝐷 ∈ (TotBnd‘𝐵))

Distinct variable groups:   𝑥,𝑅   𝑥,𝐵   𝜑,𝑥   𝑥,𝐼   𝑥,𝑆   𝑥,𝑌

Allowed substitution hints:   𝐷(𝑥)   𝐸(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem prdstotbnd

Dummy variables 𝑧 𝑟 𝑓 𝑔 𝑣 𝑦 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2622	. . . 4 ⊢ (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
2		eqid 2622	. . . 4 ⊢ (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
3		prdsbnd.v	. . . 4 ⊢ 𝑉 = (Base‘(𝑅‘𝑥))
4		prdsbnd.e	. . . 4 ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉))
5		eqid 2622	. . . 4 ⊢ (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
6		prdsbnd.s	. . . 4 ⊢ (𝜑 → 𝑆 ∈ 𝑊)
7		prdsbnd.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ Fin)
8		fvexd 6203	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V)
9		prdstotbnd.m	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (TotBnd‘𝑉))
10		totbndmet 33571	. . . . 5 ⊢ (𝐸 ∈ (TotBnd‘𝑉) → 𝐸 ∈ (Met‘𝑉))
11	9, 10	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉))
12	1, 2, 3, 4, 5, 6, 7, 8, 11	prdsmet 22175	. . 3 ⊢ (𝜑 → (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) ∈ (Met‘(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))))
13		prdsbnd.d	. . . 4 ⊢ 𝐷 = (dist‘𝑌)
14		prdsbnd.y	. . . . . 6 ⊢ 𝑌 = (𝑆Xs𝑅)
15		prdsbnd.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 Fn 𝐼)
16		dffn5 6241	. . . . . . . 8 ⊢ (𝑅 Fn 𝐼 ↔ 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
17	15, 16	sylib 208	. . . . . . 7 ⊢ (𝜑 → 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
18	17	oveq2d 6666	. . . . . 6 ⊢ (𝜑 → (𝑆Xs𝑅) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
19	14, 18	syl5eq 2668	. . . . 5 ⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))
20	19	fveq2d 6195	. . . 4 ⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
21	13, 20	syl5eq 2668	. . 3 ⊢ (𝜑 → 𝐷 = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
22		prdsbnd.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑌)
23	19	fveq2d 6195	. . . . 5 ⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
24	22, 23	syl5eq 2668	. . . 4 ⊢ (𝜑 → 𝐵 = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))
25	24	fveq2d 6195	. . 3 ⊢ (𝜑 → (Met‘𝐵) = (Met‘(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))))
26	12, 21, 25	3eltr4d 2716	. 2 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵))
27	7	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝐼 ∈ Fin)
28		istotbnd3 33570	. . . . . . . . . . 11 ⊢ (𝐸 ∈ (TotBnd‘𝑉) ↔ (𝐸 ∈ (Met‘𝑉) ∧ ∀𝑟 ∈ ℝ+ ∃𝑤 ∈ (𝒫 𝑉 ∩ Fin)∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
29	28	simprbi 480	. . . . . . . . . 10 ⊢ (𝐸 ∈ (TotBnd‘𝑉) → ∀𝑟 ∈ ℝ+ ∃𝑤 ∈ (𝒫 𝑉 ∩ Fin)∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)
30	9, 29	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∀𝑟 ∈ ℝ+ ∃𝑤 ∈ (𝒫 𝑉 ∩ Fin)∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)
31	30	r19.21bi 2932	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ (𝒫 𝑉 ∩ Fin)∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)
32		df-rex 2918	. . . . . . . . 9 ⊢ (∃𝑤 ∈ (𝒫 𝑉 ∩ Fin)∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 ↔ ∃𝑤(𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
33		rexv 3220	. . . . . . . . 9 ⊢ (∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉) ↔ ∃𝑤(𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
34	32, 33	bitr4i 267	. . . . . . . 8 ⊢ (∃𝑤 ∈ (𝒫 𝑉 ∩ Fin)∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 ↔ ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
35	31, 34	sylib 208	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
36	35	an32s 846	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑥 ∈ 𝐼) → ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
37	36	ralrimiva 2966	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉))
38		eleq1 2689	. . . . . . 7 ⊢ (𝑤 = (𝑓‘𝑥) → (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ↔ (𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin)))
39		iuneq1 4534	. . . . . . . 8 ⊢ (𝑤 = (𝑓‘𝑥) → ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟))
40	39	eqeq1d 2624	. . . . . . 7 ⊢ (𝑤 = (𝑓‘𝑥) → (∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 ↔ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))
41	38, 40	anbi12d 747	. . . . . 6 ⊢ (𝑤 = (𝑓‘𝑥) → ((𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉) ↔ ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉)))
42	41	ac6sfi 8204	. . . . 5 ⊢ ((𝐼 ∈ Fin ∧ ∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)) → ∃𝑓(𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉)))
43	27, 37, 42	syl2anc 693	. . . 4 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ∃𝑓(𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉)))
44		elfpw 8268	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ↔ ((𝑓‘𝑥) ⊆ 𝑉 ∧ (𝑓‘𝑥) ∈ Fin))
45	44	simplbi 476	. . . . . . . . . . 11 ⊢ ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) → (𝑓‘𝑥) ⊆ 𝑉)
46	45	adantr 481	. . . . . . . . . 10 ⊢ (((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (𝑓‘𝑥) ⊆ 𝑉)
47	46	ralimi 2952	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ 𝑉)
48	47	ad2antll 765	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ 𝑉)
49		ss2ixp 7921	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ 𝑉 → X𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ X𝑥 ∈ 𝐼 𝑉)
50	48, 49	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ X𝑥 ∈ 𝐼 𝑉)
51		fnfi 8238	. . . . . . . . . . 11 ⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → 𝑅 ∈ Fin)
52	15, 7, 51	syl2anc 693	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Fin)
53		fndm 5990	. . . . . . . . . . 11 ⊢ (𝑅 Fn 𝐼 → dom 𝑅 = 𝐼)
54	15, 53	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → dom 𝑅 = 𝐼)
55	14, 6, 52, 22, 54	prdsbas 16117	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
56	3	rgenw 2924	. . . . . . . . . 10 ⊢ ∀𝑥 ∈ 𝐼 𝑉 = (Base‘(𝑅‘𝑥))
57		ixpeq2 7922	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐼 𝑉 = (Base‘(𝑅‘𝑥)) → X𝑥 ∈ 𝐼 𝑉 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
58	56, 57	ax-mp 5	. . . . . . . . 9 ⊢ X𝑥 ∈ 𝐼 𝑉 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥))
59	55, 58	syl6eqr 2674	. . . . . . . 8 ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 𝑉)
60	59	ad2antrr 762	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐵 = X𝑥 ∈ 𝐼 𝑉)
61	50, 60	sseqtr4d 3642	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ 𝐵)
62	27	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐼 ∈ Fin)
63	44	simprbi 480	. . . . . . . . . 10 ⊢ ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) → (𝑓‘𝑥) ∈ Fin)
64	63	adantr 481	. . . . . . . . 9 ⊢ (((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (𝑓‘𝑥) ∈ Fin)
65	64	ralimi 2952	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ Fin)
66	65	ad2antll 765	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ Fin)
67		ixpfi 8263	. . . . . . 7 ⊢ ((𝐼 ∈ Fin ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ Fin) → X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ Fin)
68	62, 66, 67	syl2anc 693	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ Fin)
69		elfpw 8268	. . . . . 6 ⊢ (X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ (𝒫 𝐵 ∩ Fin) ↔ (X𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ 𝐵 ∧ X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ Fin))
70	61, 68, 69	sylanbrc 698	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ (𝒫 𝐵 ∩ Fin))
71		metxmet 22139	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵))
72	26, 71	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵))
73		rpxr 11840	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
74		blssm 22223	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
75	74	3expa 1265	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
76	75	an32s 846	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑟 ∈ ℝ*) ∧ 𝑦 ∈ 𝐵) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
77	76	ralrimiva 2966	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑟 ∈ ℝ*) → ∀𝑦 ∈ 𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
78	72, 73, 77	syl2an 494	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ∀𝑦 ∈ 𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
79	78	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑦 ∈ 𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
80		ssralv 3666	. . . . . . . 8 ⊢ (X𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ 𝐵 → (∀𝑦 ∈ 𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵 → ∀𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵))
81	61, 79, 80	sylc 65	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
82		iunss 4561	. . . . . . 7 ⊢ (∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵 ↔ ∀𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
83	81, 82	sylibr 224	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)
84	62	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → 𝐼 ∈ Fin)
85	60	eleq2d 2687	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔 ∈ 𝐵 ↔ 𝑔 ∈ X𝑥 ∈ 𝐼 𝑉))
86		vex 3203	. . . . . . . . . . . . . . . 16 ⊢ 𝑔 ∈ V
87	86	elixp 7915	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∈ X𝑥 ∈ 𝐼 𝑉 ↔ (𝑔 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉))
88	87	simprbi 480	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ X𝑥 ∈ 𝐼 𝑉 → ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉)
89		df-rex 2918	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑧 ∈ (𝑓‘𝑥)(𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧(𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
90		eliun 4524	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔‘𝑥) ∈ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧 ∈ (𝑓‘𝑥)(𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟))
91		rexv 3220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ ∃𝑧(𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
92	89, 90, 91	3bitr4i 292	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔‘𝑥) ∈ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
93		eleq2 2690	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → ((𝑔‘𝑥) ∈ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) ↔ (𝑔‘𝑥) ∈ 𝑉))
94	92, 93	syl5bbr 274	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → (∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ (𝑔‘𝑥) ∈ 𝑉))
95	94	biimprd 238	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → ((𝑔‘𝑥) ∈ 𝑉 → ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
96	95	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ((𝑔‘𝑥) ∈ 𝑉 → ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
97	96	ral2imi 2947	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉 → ∀𝑥 ∈ 𝐼 ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
98	97	ad2antll 765	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉 → ∀𝑥 ∈ 𝐼 ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
99	88, 98	syl5 34	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔 ∈ X𝑥 ∈ 𝐼 𝑉 → ∀𝑥 ∈ 𝐼 ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
100	85, 99	sylbid 230	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔 ∈ 𝐵 → ∀𝑥 ∈ 𝐼 ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟))))
101	100	imp 445	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → ∀𝑥 ∈ 𝐼 ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))
102		eleq1 2689	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝑦‘𝑥) → (𝑧 ∈ (𝑓‘𝑥) ↔ (𝑦‘𝑥) ∈ (𝑓‘𝑥)))
103		oveq1 6657	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑦‘𝑥) → (𝑧(ball‘𝐸)𝑟) = ((𝑦‘𝑥)(ball‘𝐸)𝑟))
104	103	eleq2d 2687	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝑦‘𝑥) → ((𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟) ↔ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))
105	102, 104	anbi12d 747	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑦‘𝑥) → ((𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))))
106	105	ac6sfi 8204	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ Fin ∧ ∀𝑥 ∈ 𝐼 ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟))) → ∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))))
107	84, 101, 106	syl2anc 693	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → ∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))))
108		ffn 6045	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦:𝐼⟶V → 𝑦 Fn 𝐼)
109		simpl 473	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)) → (𝑦‘𝑥) ∈ (𝑓‘𝑥))
110	109	ralimi 2952	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)) → ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ (𝑓‘𝑥))
111	108, 110	anim12i 590	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))) → (𝑦 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ (𝑓‘𝑥)))
112		vex 3203	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
113	112	elixp 7915	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ X𝑥 ∈ 𝐼 (𝑓‘𝑥) ↔ (𝑦 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ (𝑓‘𝑥)))
114	111, 113	sylibr 224	. . . . . . . . . . . . . . 15 ⊢ ((𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))) → 𝑦 ∈ X𝑥 ∈ 𝐼 (𝑓‘𝑥))
115	114	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑦 ∈ X𝑥 ∈ 𝐼 (𝑓‘𝑥))
116	85	biimpa 501	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ X𝑥 ∈ 𝐼 𝑉)
117		ixpfn 7914	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ X𝑥 ∈ 𝐼 𝑉 → 𝑔 Fn 𝐼)
118	116, 117	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → 𝑔 Fn 𝐼)
119	118	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑔 Fn 𝐼)
120		simpr 477	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)) → (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))
121	120	ralimi 2952	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)) → ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))
122	121	ad2antll 765	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))
123	86	elixp 7915	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ X𝑥 ∈ 𝐼 ((𝑦‘𝑥)(ball‘𝐸)𝑟) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))
124	119, 122, 123	sylanbrc 698	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑔 ∈ X𝑥 ∈ 𝐼 ((𝑦‘𝑥)(ball‘𝐸)𝑟))
125		simp-4l 806	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝜑)
126	50	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → X𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ X𝑥 ∈ 𝐼 𝑉)
127	126, 115	sseldd 3604	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑦 ∈ X𝑥 ∈ 𝐼 𝑉)
128	125, 59	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝐵 = X𝑥 ∈ 𝐼 𝑉)
129	127, 128	eleqtrrd 2704	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑦 ∈ 𝐵)
130		simp-4r 807	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑟 ∈ ℝ+)
131		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥))
132	131	cbvmptv 4750	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)) = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))
133	132	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))
134	19, 133	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
135	134	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
136	13, 135	syl5eq 2668	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
137	136	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ball‘𝐷) = (ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))))
138	137	oveqdr 6674	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟))
139		eqid 2622	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
140		eqid 2622	. . . . . . . . . . . . . . . . . 18 ⊢ (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))
141	6	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑆 ∈ 𝑊)
142	7	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ Fin)
143		fvexd 6203	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V)
144		metxmet 22139	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉))
145	11, 144	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
146	145	adantlr 751	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))
147		simprl 794	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑦 ∈ 𝐵)
148	134	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
149	22, 148	syl5eq 2668	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
150	149	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝐵 = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
151	147, 150	eleqtrd 2703	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑦 ∈ (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))
152	73	ad2antll 765	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ*)
153		rpgt0 11844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 ∈ ℝ+ → 0 < 𝑟)
154	153	ad2antll 765	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 0 < 𝑟)
155	133, 139, 3, 4, 140, 141, 142, 143, 146, 151, 152, 154	prdsbl 22296	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟) = X𝑥 ∈ 𝐼 ((𝑦‘𝑥)(ball‘𝐸)𝑟))
156	138, 155	eqtrd 2656	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘𝐷)𝑟) = X𝑥 ∈ 𝐼 ((𝑦‘𝑥)(ball‘𝐸)𝑟))
157	125, 129, 130, 156	syl12anc 1324	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → (𝑦(ball‘𝐷)𝑟) = X𝑥 ∈ 𝐼 ((𝑦‘𝑥)(ball‘𝐸)𝑟))
158	124, 157	eleqtrrd 2704	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))
159	115, 158	jca 554	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → (𝑦 ∈ X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
160	159	ex 450	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → ((𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))) → (𝑦 ∈ X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))))
161	160	eximdv 1846	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → (∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))) → ∃𝑦(𝑦 ∈ X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))))
162		df-rex 2918	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦(𝑦 ∈ X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
163	161, 162	syl6ibr 242	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → (∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))) → ∃𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
164	107, 163	mpd 15	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → ∃𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟))
165	164	ex 450	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔 ∈ 𝐵 → ∃𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))
166		eliun 4524	. . . . . . . 8 ⊢ (𝑔 ∈ ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟))
167	165, 166	syl6ibr 242	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔 ∈ 𝐵 → 𝑔 ∈ ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟)))
168	167	ssrdv 3609	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐵 ⊆ ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟))
169	83, 168	eqssd 3620	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵)
170		iuneq1 4534	. . . . . . 7 ⊢ (𝑣 = X𝑥 ∈ 𝐼 (𝑓‘𝑥) → ∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟))
171	170	eqeq1d 2624	. . . . . 6 ⊢ (𝑣 = X𝑥 ∈ 𝐼 (𝑓‘𝑥) → (∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵 ↔ ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵))
172	171	rspcev 3309	. . . . 5 ⊢ ((X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ (𝒫 𝐵 ∩ Fin) ∧ ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin)∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
173	70, 169, 172	syl2anc 693	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin)∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
174	43, 173	exlimddv 1863	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin)∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
175	174	ralrimiva 2966	. 2 ⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin)∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)
176		istotbnd3 33570	. 2 ⊢ (𝐷 ∈ (TotBnd‘𝐵) ↔ (𝐷 ∈ (Met‘𝐵) ∧ ∀𝑟 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin)∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵))
177	26, 175, 176	sylanbrc 698	1 ⊢ (𝜑 → 𝐷 ∈ (TotBnd‘𝐵))

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913  Vcvv 3200   ∩ cin 3573   ⊆ wss 3574  𝒫 cpw 4158  ∪ ciun 4520   class class class wbr 4653   ↦ cmpt 4729   × cxp 5112  dom cdm 5114   ↾ cres 5116   Fn wfn 5883  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650  Xcixp 7908  Fincfn 7955  0cc0 9936  ℝ^*cxr 10073   < clt 10074  ℝ⁺crp 11832  Basecbs 15857  distcds 15950  X_scprds 16106  ∞Metcxmt 19731  Metcme 19732  ballcbl 19733  TotBndctotbnd 33565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-icc 12182  df-fz 12327  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-plusg 15954  df-mulr 15955  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-hom 15966  df-cco 15967  df-prds 16108  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-totbnd 33567

This theorem is referenced by:  prdsbnd2  33594