prdstotbnd

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)

	Ref	Expression
Hypotheses	prdsbnd.y	$⊢ Y = S ⨉_{𝑠} R$
	prdsbnd.b	$⊢ B = {Base}_{Y}$
	prdsbnd.v	$⊢ V = {Base}_{R (x)}$
	prdsbnd.e	$⊢ E = {dist (R (x)) ↾}_{(V \times V)}$
	prdsbnd.d	$⊢ D = dist (Y)$
	prdsbnd.s	$⊢ φ \to S \in W$
	prdsbnd.i	$⊢ φ \to I \in Fin$
	prdsbnd.r	$⊢ φ \to R Fn I$
	prdstotbnd.m	$⊢ (φ \land x \in I) \to E \in TotBnd (V)$
Assertion	prdstotbnd	$⊢ φ \to D \in TotBnd (B)$

Proof

Step	Hyp	Ref	Expression
1		prdsbnd.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdsbnd.b	$⊢ B = {Base}_{Y}$
3		prdsbnd.v	$⊢ V = {Base}_{R (x)}$
4		prdsbnd.e	$⊢ E = {dist (R (x)) ↾}_{(V \times V)}$
5		prdsbnd.d	$⊢ D = dist (Y)$
6		prdsbnd.s	$⊢ φ \to S \in W$
7		prdsbnd.i	$⊢ φ \to I \in Fin$
8		prdsbnd.r	$⊢ φ \to R Fn I$
9		prdstotbnd.m	$⊢ (φ \land x \in I) \to E \in TotBnd (V)$
10		eqid	$⊢ S ⨉_{𝑠} (x \in I ⟼ R (x)) = S ⨉_{𝑠} (x \in I ⟼ R (x))$
11		eqid	$⊢ {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))} = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
12		eqid	$⊢ dist (S ⨉_{𝑠} (x \in I ⟼ R (x))) = dist (S ⨉_{𝑠} (x \in I ⟼ R (x)))$
13		fvexd	$⊢ (φ \land x \in I) \to R (x) \in V$
14		totbndmet	$⊢ E \in TotBnd (V) \to E \in Met (V)$
15	9 14	syl	$⊢ (φ \land x \in I) \to E \in Met (V)$
16	10 11 3 4 12 6 7 13 15	prdsmet	$⊢ φ \to dist (S ⨉_{𝑠} (x \in I ⟼ R (x))) \in Met ({Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))})$
17		dffn5	$⊢ R Fn I \leftrightarrow R = (x \in I ⟼ R (x))$
18	8 17	sylib	$⊢ φ \to R = (x \in I ⟼ R (x))$
19	18	oveq2d	$⊢ φ \to S ⨉_{𝑠} R = S ⨉_{𝑠} (x \in I ⟼ R (x))$
20	1 19	syl5eq	$⊢ φ \to Y = S ⨉_{𝑠} (x \in I ⟼ R (x))$
21	20	fveq2d	$⊢ φ \to dist (Y) = dist (S ⨉_{𝑠} (x \in I ⟼ R (x)))$
22	5 21	syl5eq	$⊢ φ \to D = dist (S ⨉_{𝑠} (x \in I ⟼ R (x)))$
23	20	fveq2d	$⊢ φ \to {Base}_{Y} = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
24	2 23	syl5eq	$⊢ φ \to B = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
25	24	fveq2d	$⊢ φ \to Met (B) = Met ({Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))})$
26	16 22 25	3eltr4d	$⊢ φ \to D \in Met (B)$
27	7	adantr	$⊢ (φ \land r \in ℝ^{+}) \to I \in Fin$
28		istotbnd3	$⊢ E \in TotBnd (V) \leftrightarrow (E \in Met (V) \land \forall r \in ℝ^{+} \exists w \in (𝒫 V \cap Fin) ⋃_{z \in w} (z ball (E) r) = V)$
29	28	simprbi	$⊢ E \in TotBnd (V) \to \forall r \in ℝ^{+} \exists w \in (𝒫 V \cap Fin) ⋃_{z \in w} (z ball (E) r) = V$
30	9 29	syl	$⊢ (φ \land x \in I) \to \forall r \in ℝ^{+} \exists w \in (𝒫 V \cap Fin) ⋃_{z \in w} (z ball (E) r) = V$
31	30	r19.21bi	$⊢ ((φ \land x \in I) \land r \in ℝ^{+}) \to \exists w \in (𝒫 V \cap Fin) ⋃_{z \in w} (z ball (E) r) = V$
32		df-rex	$⊢ \exists w \in (𝒫 V \cap Fin) ⋃_{z \in w} (z ball (E) r) = V \leftrightarrow \exists w (w \in (𝒫 V \cap Fin) \land ⋃_{z \in w} (z ball (E) r) = V)$
33		rexv	$⊢ \exists w \in V (w \in (𝒫 V \cap Fin) \land ⋃_{z \in w} (z ball (E) r) = V) \leftrightarrow \exists w (w \in (𝒫 V \cap Fin) \land ⋃_{z \in w} (z ball (E) r) = V)$
34	32 33	bitr4i	$⊢ \exists w \in (𝒫 V \cap Fin) ⋃_{z \in w} (z ball (E) r) = V \leftrightarrow \exists w \in V (w \in (𝒫 V \cap Fin) \land ⋃_{z \in w} (z ball (E) r) = V)$
35	31 34	sylib	$⊢ ((φ \land x \in I) \land r \in ℝ^{+}) \to \exists w \in V (w \in (𝒫 V \cap Fin) \land ⋃_{z \in w} (z ball (E) r) = V)$
36	35	an32s	$⊢ ((φ \land r \in ℝ^{+}) \land x \in I) \to \exists w \in V (w \in (𝒫 V \cap Fin) \land ⋃_{z \in w} (z ball (E) r) = V)$
37	36	ralrimiva	$⊢ (φ \land r \in ℝ^{+}) \to \forall x \in I \exists w \in V (w \in (𝒫 V \cap Fin) \land ⋃_{z \in w} (z ball (E) r) = V)$
38		eleq1	$⊢ w = f (x) \to (w \in (𝒫 V \cap Fin) \leftrightarrow f (x) \in (𝒫 V \cap Fin))$
39		iuneq1	$⊢ w = f (x) \to ⋃_{z \in w} (z ball (E) r) = ⋃_{z \in f (x)} (z ball (E) r)$
40	39	eqeq1d	$⊢ w = f (x) \to (⋃_{z \in w} (z ball (E) r) = V \leftrightarrow ⋃_{z \in f (x)} (z ball (E) r) = V)$
41	38 40	anbi12d	$⊢ w = f (x) \to ((w \in (𝒫 V \cap Fin) \land ⋃_{z \in w} (z ball (E) r) = V) \leftrightarrow (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))$
42	41	ac6sfi	$⊢ (I \in Fin \land \forall x \in I \exists w \in V (w \in (𝒫 V \cap Fin) \land ⋃_{z \in w} (z ball (E) r) = V)) \to \exists f (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))$
43	27 37 42	syl2anc	$⊢ (φ \land r \in ℝ^{+}) \to \exists f (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))$
44		elfpw	$⊢ f (x) \in (𝒫 V \cap Fin) \leftrightarrow (f (x) \subseteq V \land f (x) \in Fin)$
45	44	simplbi	$⊢ f (x) \in (𝒫 V \cap Fin) \to f (x) \subseteq V$
46	45	adantr	$⊢ (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V) \to f (x) \subseteq V$
47	46	ralimi	$⊢ \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V) \to \forall x \in I f (x) \subseteq V$
48	47	ad2antll	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to \forall x \in I f (x) \subseteq V$
49		ss2ixp	$⊢ \forall x \in I f (x) \subseteq V \to \underset{x \in I}{⨉} f (x) \subseteq \underset{x \in I}{⨉} V$
50	48 49	syl	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to \underset{x \in I}{⨉} f (x) \subseteq \underset{x \in I}{⨉} V$
51		fnfi	$⊢ (R Fn I \land I \in Fin) \to R \in Fin$
52	8 7 51	syl2anc	$⊢ φ \to R \in Fin$
53		fndm	$⊢ R Fn I \to dom R = I$
54	8 53	syl	$⊢ φ \to dom R = I$
55	1 6 52 2 54	prdsbas	$⊢ φ \to B = \underset{x \in I}{⨉} {Base}_{R (x)}$
56	3	rgenw	$⊢ \forall x \in I V = {Base}_{R (x)}$
57		ixpeq2	$⊢ \forall x \in I V = {Base}_{R (x)} \to \underset{x \in I}{⨉} V = \underset{x \in I}{⨉} {Base}_{R (x)}$
58	56 57	ax-mp	$⊢ \underset{x \in I}{⨉} V = \underset{x \in I}{⨉} {Base}_{R (x)}$
59	55 58	syl6eqr	$⊢ φ \to B = \underset{x \in I}{⨉} V$
60	59	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to B = \underset{x \in I}{⨉} V$
61	50 60	sseqtrrd	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to \underset{x \in I}{⨉} f (x) \subseteq B$
62	27	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to I \in Fin$
63	44	simprbi	$⊢ f (x) \in (𝒫 V \cap Fin) \to f (x) \in Fin$
64	63	adantr	$⊢ (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V) \to f (x) \in Fin$
65	64	ralimi	$⊢ \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V) \to \forall x \in I f (x) \in Fin$
66	65	ad2antll	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to \forall x \in I f (x) \in Fin$
67		ixpfi	$⊢ (I \in Fin \land \forall x \in I f (x) \in Fin) \to \underset{x \in I}{⨉} f (x) \in Fin$
68	62 66 67	syl2anc	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to \underset{x \in I}{⨉} f (x) \in Fin$
69		elfpw	$⊢ \underset{x \in I}{⨉} f (x) \in (𝒫 B \cap Fin) \leftrightarrow (\underset{x \in I}{⨉} f (x) \subseteq B \land \underset{x \in I}{⨉} f (x) \in Fin)$
70	61 68 69	sylanbrc	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to \underset{x \in I}{⨉} f (x) \in (𝒫 B \cap Fin)$
71		metxmet	$⊢ D \in Met (B) \to D \in ∞Met (B)$
72	26 71	syl	$⊢ φ \to D \in ∞Met (B)$
73		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
74		blssm	$⊢ (D \in ∞Met (B) \land y \in B \land r \in ℝ^{*}) \to y ball (D) r \subseteq B$
75	74	3expa	$⊢ ((D \in ∞Met (B) \land y \in B) \land r \in ℝ^{*}) \to y ball (D) r \subseteq B$
76	75	an32s	$⊢ ((D \in ∞Met (B) \land r \in ℝ^{*}) \land y \in B) \to y ball (D) r \subseteq B$
77	76	ralrimiva	$⊢ (D \in ∞Met (B) \land r \in ℝ^{*}) \to \forall y \in B y ball (D) r \subseteq B$
78	72 73 77	syl2an	$⊢ (φ \land r \in ℝ^{+}) \to \forall y \in B y ball (D) r \subseteq B$
79	78	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to \forall y \in B y ball (D) r \subseteq B$
80		ssralv	$⊢ \underset{x \in I}{⨉} f (x) \subseteq B \to (\forall y \in B y ball (D) r \subseteq B \to \forall y \in \underset{x \in I}{⨉} f (x) y ball (D) r \subseteq B)$
81	61 79 80	sylc	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to \forall y \in \underset{x \in I}{⨉} f (x) y ball (D) r \subseteq B$
82		iunss	$⊢ ⋃_{y \in \underset{x \in I}{⨉} f (x)} (y ball (D) r) \subseteq B \leftrightarrow \forall y \in \underset{x \in I}{⨉} f (x) y ball (D) r \subseteq B$
83	81 82	sylibr	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to ⋃_{y \in \underset{x \in I}{⨉} f (x)} (y ball (D) r) \subseteq B$
84	62	adantr	$⊢ (((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \to I \in Fin$
85	60	eleq2d	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to (g \in B \leftrightarrow g \in \underset{x \in I}{⨉} V)$
86		vex	$⊢ g \in V$
87	86	elixp	$⊢ g \in \underset{x \in I}{⨉} V \leftrightarrow (g Fn I \land \forall x \in I g (x) \in V)$
88	87	simprbi	$⊢ g \in \underset{x \in I}{⨉} V \to \forall x \in I g (x) \in V$
89		df-rex	$⊢ \exists z \in f (x) g (x) \in (z ball (E) r) \leftrightarrow \exists z (z \in f (x) \land g (x) \in (z ball (E) r))$
90		eliun	$⊢ g (x) \in ⋃_{z \in f (x)} (z ball (E) r) \leftrightarrow \exists z \in f (x) g (x) \in (z ball (E) r)$
91		rexv	$⊢ \exists z \in V (z \in f (x) \land g (x) \in (z ball (E) r)) \leftrightarrow \exists z (z \in f (x) \land g (x) \in (z ball (E) r))$
92	89 90 91	3bitr4i	$⊢ g (x) \in ⋃_{z \in f (x)} (z ball (E) r) \leftrightarrow \exists z \in V (z \in f (x) \land g (x) \in (z ball (E) r))$
93		eleq2	$⊢ ⋃_{z \in f (x)} (z ball (E) r) = V \to (g (x) \in ⋃_{z \in f (x)} (z ball (E) r) \leftrightarrow g (x) \in V)$
94	92 93	bitr3id	$⊢ ⋃_{z \in f (x)} (z ball (E) r) = V \to (\exists z \in V (z \in f (x) \land g (x) \in (z ball (E) r)) \leftrightarrow g (x) \in V)$
95	94	biimprd	$⊢ ⋃_{z \in f (x)} (z ball (E) r) = V \to (g (x) \in V \to \exists z \in V (z \in f (x) \land g (x) \in (z ball (E) r)))$
96	95	adantl	$⊢ (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V) \to (g (x) \in V \to \exists z \in V (z \in f (x) \land g (x) \in (z ball (E) r)))$
97	96	ral2imi	$⊢ \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V) \to (\forall x \in I g (x) \in V \to \forall x \in I \exists z \in V (z \in f (x) \land g (x) \in (z ball (E) r)))$
98	97	ad2antll	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to (\forall x \in I g (x) \in V \to \forall x \in I \exists z \in V (z \in f (x) \land g (x) \in (z ball (E) r)))$
99	88 98	syl5	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to (g \in \underset{x \in I}{⨉} V \to \forall x \in I \exists z \in V (z \in f (x) \land g (x) \in (z ball (E) r)))$
100	85 99	sylbid	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to (g \in B \to \forall x \in I \exists z \in V (z \in f (x) \land g (x) \in (z ball (E) r)))$
101	100	imp	$⊢ (((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \to \forall x \in I \exists z \in V (z \in f (x) \land g (x) \in (z ball (E) r))$
102		eleq1	$⊢ z = y (x) \to (z \in f (x) \leftrightarrow y (x) \in f (x))$
103		oveq1	$⊢ z = y (x) \to z ball (E) r = y (x) ball (E) r$
104	103	eleq2d	$⊢ z = y (x) \to (g (x) \in (z ball (E) r) \leftrightarrow g (x) \in (y (x) ball (E) r))$
105	102 104	anbi12d	$⊢ z = y (x) \to ((z \in f (x) \land g (x) \in (z ball (E) r)) \leftrightarrow (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))$
106	105	ac6sfi	$⊢ (I \in Fin \land \forall x \in I \exists z \in V (z \in f (x) \land g (x) \in (z ball (E) r))) \to \exists y (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))$
107	84 101 106	syl2anc	$⊢ (((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \to \exists y (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))$
108		ffn	$⊢ y : I ⟶ V \to y Fn I$
109		simpl	$⊢ (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)) \to y (x) \in f (x)$
110	109	ralimi	$⊢ \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)) \to \forall x \in I y (x) \in f (x)$
111	108 110	anim12i	$⊢ (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r))) \to (y Fn I \land \forall x \in I y (x) \in f (x))$
112		vex	$⊢ y \in V$
113	112	elixp	$⊢ y \in \underset{x \in I}{⨉} f (x) \leftrightarrow (y Fn I \land \forall x \in I y (x) \in f (x))$
114	111 113	sylibr	$⊢ (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r))) \to y \in \underset{x \in I}{⨉} f (x)$
115	114	adantl	$⊢ ((((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \land (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))) \to y \in \underset{x \in I}{⨉} f (x)$
116	85	biimpa	$⊢ (((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \to g \in \underset{x \in I}{⨉} V$
117		ixpfn	$⊢ g \in \underset{x \in I}{⨉} V \to g Fn I$
118	116 117	syl	$⊢ (((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \to g Fn I$
119	118	adantr	$⊢ ((((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \land (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))) \to g Fn I$
120		simpr	$⊢ (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)) \to g (x) \in (y (x) ball (E) r)$
121	120	ralimi	$⊢ \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)) \to \forall x \in I g (x) \in (y (x) ball (E) r)$
122	121	ad2antll	$⊢ ((((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \land (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))) \to \forall x \in I g (x) \in (y (x) ball (E) r)$
123	86	elixp	$⊢ g \in \underset{x \in I}{⨉} (y (x) ball (E) r) \leftrightarrow (g Fn I \land \forall x \in I g (x) \in (y (x) ball (E) r))$
124	119 122 123	sylanbrc	$⊢ ((((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \land (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))) \to g \in \underset{x \in I}{⨉} (y (x) ball (E) r)$
125		simp-4l	$⊢ ((((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \land (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))) \to φ$
126	50	ad2antrr	$⊢ ((((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \land (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))) \to \underset{x \in I}{⨉} f (x) \subseteq \underset{x \in I}{⨉} V$
127	126 115	sseldd	$⊢ ((((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \land (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))) \to y \in \underset{x \in I}{⨉} V$
128	125 59	syl	$⊢ ((((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \land (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))) \to B = \underset{x \in I}{⨉} V$
129	127 128	eleqtrrd	$⊢ ((((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \land (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))) \to y \in B$
130		simp-4r	$⊢ ((((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \land (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))) \to r \in ℝ^{+}$
131		fveq2	$⊢ y = x \to R (y) = R (x)$
132	131	cbvmptv	$⊢ (y \in I ⟼ R (y)) = (x \in I ⟼ R (x))$
133	132	oveq2i	$⊢ S ⨉_{𝑠} (y \in I ⟼ R (y)) = S ⨉_{𝑠} (x \in I ⟼ R (x))$
134	20 133	syl6eqr	$⊢ φ \to Y = S ⨉_{𝑠} (y \in I ⟼ R (y))$
135	134	fveq2d	$⊢ φ \to dist (Y) = dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))$
136	5 135	syl5eq	$⊢ φ \to D = dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))$
137	136	fveq2d	$⊢ φ \to ball (D) = ball (dist (S ⨉_{𝑠} (y \in I ⟼ R (y))))$
138	137	oveqdr	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to y ball (D) r = y ball (dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))) r$
139		eqid	$⊢ {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))} = {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
140		eqid	$⊢ dist (S ⨉_{𝑠} (y \in I ⟼ R (y))) = dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))$
141	6	adantr	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to S \in W$
142	7	adantr	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to I \in Fin$
143		fvexd	$⊢ ((φ \land (y \in B \land r \in ℝ^{+})) \land x \in I) \to R (x) \in V$
144		metxmet	$⊢ E \in Met (V) \to E \in ∞Met (V)$
145	15 144	syl	$⊢ (φ \land x \in I) \to E \in ∞Met (V)$
146	145	adantlr	$⊢ ((φ \land (y \in B \land r \in ℝ^{+})) \land x \in I) \to E \in ∞Met (V)$
147		simprl	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to y \in B$
148	134	fveq2d	$⊢ φ \to {Base}_{Y} = {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
149	2 148	syl5eq	$⊢ φ \to B = {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
150	149	adantr	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to B = {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
151	147 150	eleqtrd	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to y \in {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
152	73	ad2antll	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to r \in ℝ^{*}$
153		rpgt0	$⊢ r \in ℝ^{+} \to 0 < r$
154	153	ad2antll	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to 0 < r$
155	133 139 3 4 140 141 142 143 146 151 152 154	prdsbl	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to y ball (dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))) r = \underset{x \in I}{⨉} (y (x) ball (E) r)$
156	138 155	eqtrd	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to y ball (D) r = \underset{x \in I}{⨉} (y (x) ball (E) r)$
157	125 129 130 156	syl12anc	$⊢ ((((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \land (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))) \to y ball (D) r = \underset{x \in I}{⨉} (y (x) ball (E) r)$
158	124 157	eleqtrrd	$⊢ ((((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \land (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))) \to g \in (y ball (D) r)$
159	115 158	jca	$⊢ ((((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \land (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)))) \to (y \in \underset{x \in I}{⨉} f (x) \land g \in (y ball (D) r))$
160	159	ex	$⊢ (((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \to ((y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r))) \to (y \in \underset{x \in I}{⨉} f (x) \land g \in (y ball (D) r)))$
161	160	eximdv	$⊢ (((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \to (\exists y (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r))) \to \exists y (y \in \underset{x \in I}{⨉} f (x) \land g \in (y ball (D) r)))$
162		df-rex	$⊢ \exists y \in \underset{x \in I}{⨉} f (x) g \in (y ball (D) r) \leftrightarrow \exists y (y \in \underset{x \in I}{⨉} f (x) \land g \in (y ball (D) r))$
163	161 162	syl6ibr	$⊢ (((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \to (\exists y (y : I ⟶ V \land \forall x \in I (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r))) \to \exists y \in \underset{x \in I}{⨉} f (x) g \in (y ball (D) r))$
164	107 163	mpd	$⊢ (((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \land g \in B) \to \exists y \in \underset{x \in I}{⨉} f (x) g \in (y ball (D) r)$
165	164	ex	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to (g \in B \to \exists y \in \underset{x \in I}{⨉} f (x) g \in (y ball (D) r))$
166		eliun	$⊢ g \in ⋃_{y \in \underset{x \in I}{⨉} f (x)} (y ball (D) r) \leftrightarrow \exists y \in \underset{x \in I}{⨉} f (x) g \in (y ball (D) r)$
167	165 166	syl6ibr	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to (g \in B \to g \in ⋃_{y \in \underset{x \in I}{⨉} f (x)} (y ball (D) r))$
168	167	ssrdv	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to B \subseteq ⋃_{y \in \underset{x \in I}{⨉} f (x)} (y ball (D) r)$
169	83 168	eqssd	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to ⋃_{y \in \underset{x \in I}{⨉} f (x)} (y ball (D) r) = B$
170		iuneq1	$⊢ v = \underset{x \in I}{⨉} f (x) \to ⋃_{y \in v} (y ball (D) r) = ⋃_{y \in \underset{x \in I}{⨉} f (x)} (y ball (D) r)$
171	170	eqeq1d	$⊢ v = \underset{x \in I}{⨉} f (x) \to (⋃_{y \in v} (y ball (D) r) = B \leftrightarrow ⋃_{y \in \underset{x \in I}{⨉} f (x)} (y ball (D) r) = B)$
172	171	rspcev	$⊢ (\underset{x \in I}{⨉} f (x) \in (𝒫 B \cap Fin) \land ⋃_{y \in \underset{x \in I}{⨉} f (x)} (y ball (D) r) = B) \to \exists v \in (𝒫 B \cap Fin) ⋃_{y \in v} (y ball (D) r) = B$
173	70 169 172	syl2anc	$⊢ ((φ \land r \in ℝ^{+}) \land (f : I ⟶ V \land \forall x \in I (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V))) \to \exists v \in (𝒫 B \cap Fin) ⋃_{y \in v} (y ball (D) r) = B$
174	43 173	exlimddv	$⊢ (φ \land r \in ℝ^{+}) \to \exists v \in (𝒫 B \cap Fin) ⋃_{y \in v} (y ball (D) r) = B$
175	174	ralrimiva	$⊢ φ \to \forall r \in ℝ^{+} \exists v \in (𝒫 B \cap Fin) ⋃_{y \in v} (y ball (D) r) = B$
176		istotbnd3	$⊢ D \in TotBnd (B) \leftrightarrow (D \in Met (B) \land \forall r \in ℝ^{+} \exists v \in (𝒫 B \cap Fin) ⋃_{y \in v} (y ball (D) r) = B)$
177	26 175 176	sylanbrc	$⊢ φ \to D \in TotBnd (B)$

Metamath Proof Explorer

Theorem prdstotbnd

Proof