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	eqtrid	$⊢ φ \to Y = S ⨉_{𝑠} (x \in I ⟼ R (x))$
21	20	fveq2d	$⊢ φ \to dist (Y) = dist (S ⨉_{𝑠} (x \in I ⟼ R (x)))$
22	5 21	eqtrid	$⊢ φ \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	eqtrid	$⊢ φ \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	8	fndmd	$⊢ φ \to dom R = I$
54	1 6 52 2 53	prdsbas	$⊢ φ \to B = \underset{x \in I}{⨉} {Base}_{R (x)}$
55	3	rgenw	$⊢ \forall x \in I V = {Base}_{R (x)}$
56		ixpeq2	$⊢ \forall x \in I V = {Base}_{R (x)} \to \underset{x \in I}{⨉} V = \underset{x \in I}{⨉} {Base}_{R (x)}$
57	55 56	ax-mp	$⊢ \underset{x \in I}{⨉} V = \underset{x \in I}{⨉} {Base}_{R (x)}$
58	54 57	eqtr4di	$⊢ φ \to B = \underset{x \in I}{⨉} V$
59	58	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$
60	50 59	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$
61	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$
62	44	simprbi	$⊢ f (x) \in (𝒫 V \cap Fin) \to f (x) \in Fin$
63	62	adantr	$⊢ (f (x) \in (𝒫 V \cap Fin) \land ⋃_{z \in f (x)} (z ball (E) r) = V) \to f (x) \in Fin$
64	63	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$
65	64	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$
66		ixpfi	$⊢ (I \in Fin \land \forall x \in I f (x) \in Fin) \to \underset{x \in I}{⨉} f (x) \in Fin$
67	61 65 66	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$
68		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)$
69	60 67 68	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)$
70		metxmet	$⊢ D \in Met (B) \to D \in ∞Met (B)$
71	26 70	syl	$⊢ φ \to D \in ∞Met (B)$
72		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
73		blssm	$⊢ (D \in ∞Met (B) \land y \in B \land r \in ℝ^{*}) \to y ball (D) r \subseteq B$
74	73	3expa	$⊢ ((D \in ∞Met (B) \land y \in B) \land r \in ℝ^{*}) \to y ball (D) r \subseteq B$
75	74	an32s	$⊢ ((D \in ∞Met (B) \land r \in ℝ^{*}) \land y \in B) \to y ball (D) r \subseteq B$
76	75	ralrimiva	$⊢ (D \in ∞Met (B) \land r \in ℝ^{*}) \to \forall y \in B y ball (D) r \subseteq B$
77	71 72 76	syl2an	$⊢ (φ \land r \in ℝ^{+}) \to \forall y \in B y ball (D) r \subseteq B$
78	77	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$
79		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)$
80	60 78 79	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$
81		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$
82	80 81	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$
83	61	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$
84	59	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)$
85		vex	$⊢ g \in V$
86	85	elixp	$⊢ g \in \underset{x \in I}{⨉} V \leftrightarrow (g Fn I \land \forall x \in I g (x) \in V)$
87	86	simprbi	$⊢ g \in \underset{x \in I}{⨉} V \to \forall x \in I g (x) \in V$
88		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))$
89		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)$
90		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))$
91	88 89 90	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))$
92		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)$
93	91 92	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)$
94	93	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)))$
95	94	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)))$
96	95	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)))$
97	96	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)))$
98	87 97	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)))$
99	84 98	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)))$
100	99	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))$
101		eleq1	$⊢ z = y (x) \to (z \in f (x) \leftrightarrow y (x) \in f (x))$
102		oveq1	$⊢ z = y (x) \to z ball (E) r = y (x) ball (E) r$
103	102	eleq2d	$⊢ z = y (x) \to (g (x) \in (z ball (E) r) \leftrightarrow g (x) \in (y (x) ball (E) r))$
104	101 103	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)))$
105	104	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)))$
106	83 100 105	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)))$
107		ffn	$⊢ y : I ⟶ V \to y Fn I$
108		simpl	$⊢ (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)) \to y (x) \in f (x)$
109	108	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)$
110	107 109	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))$
111		vex	$⊢ y \in V$
112	111	elixp	$⊢ y \in \underset{x \in I}{⨉} f (x) \leftrightarrow (y Fn I \land \forall x \in I y (x) \in f (x))$
113	110 112	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)$
114	113	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)$
115	84	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$
116		ixpfn	$⊢ g \in \underset{x \in I}{⨉} V \to g Fn I$
117	115 116	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$
118	117	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$
119		simpr	$⊢ (y (x) \in f (x) \land g (x) \in (y (x) ball (E) r)) \to g (x) \in (y (x) ball (E) r)$
120	119	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)$
121	120	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)$
122	85	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))$
123	118 121 122	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)$
124		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 φ$
125	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$
126	125 114	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$
127	124 58	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$
128	126 127	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$
129		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 ℝ^{+}$
130		fveq2	$⊢ y = x \to R (y) = R (x)$
131	130	cbvmptv	$⊢ (y \in I ⟼ R (y)) = (x \in I ⟼ R (x))$
132	131	oveq2i	$⊢ S ⨉_{𝑠} (y \in I ⟼ R (y)) = S ⨉_{𝑠} (x \in I ⟼ R (x))$
133	20 132	eqtr4di	$⊢ φ \to Y = S ⨉_{𝑠} (y \in I ⟼ R (y))$
134	133	fveq2d	$⊢ φ \to dist (Y) = dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))$
135	5 134	eqtrid	$⊢ φ \to D = dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))$
136	135	fveq2d	$⊢ φ \to ball (D) = ball (dist (S ⨉_{𝑠} (y \in I ⟼ R (y))))$
137	136	oveqdr	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to y ball (D) r = y ball (dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))) r$
138		eqid	$⊢ {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))} = {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
139		eqid	$⊢ dist (S ⨉_{𝑠} (y \in I ⟼ R (y))) = dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))$
140	6	adantr	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to S \in W$
141	7	adantr	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to I \in Fin$
142		fvexd	$⊢ ((φ \land (y \in B \land r \in ℝ^{+})) \land x \in I) \to R (x) \in V$
143		metxmet	$⊢ E \in Met (V) \to E \in ∞Met (V)$
144	15 143	syl	$⊢ (φ \land x \in I) \to E \in ∞Met (V)$
145	144	adantlr	$⊢ ((φ \land (y \in B \land r \in ℝ^{+})) \land x \in I) \to E \in ∞Met (V)$
146		simprl	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to y \in B$
147	133	fveq2d	$⊢ φ \to {Base}_{Y} = {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
148	2 147	eqtrid	$⊢ φ \to B = {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
149	148	adantr	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to B = {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
150	146 149	eleqtrd	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to y \in {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
151	72	ad2antll	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to r \in ℝ^{*}$
152		rpgt0	$⊢ r \in ℝ^{+} \to 0 < r$
153	152	ad2antll	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to 0 < r$
154	132 138 3 4 139 140 141 142 145 150 151 153	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)$
155	137 154	eqtrd	$⊢ (φ \land (y \in B \land r \in ℝ^{+})) \to y ball (D) r = \underset{x \in I}{⨉} (y (x) ball (E) r)$
156	124 128 129 155	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)$
157	123 156	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)$
158	114 157	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))$
159	158	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)))$
160	159	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)))$
161		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))$
162	160 161	imbitrrdi	$⊢ (((φ \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))$
163	106 162	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)$
164	163	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))$
165		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)$
166	164 165	imbitrrdi	$⊢ ((φ \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))$
167	166	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)$
168	82 167	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$
169		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)$
170	169	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)$
171	170	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$
172	69 168 171	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$
173	43 172	exlimddv	$⊢ (φ \land r \in ℝ^{+}) \to \exists v \in (𝒫 B \cap Fin) ⋃_{y \in v} (y ball (D) r) = B$
174	173	ralrimiva	$⊢ φ \to \forall r \in ℝ^{+} \exists v \in (𝒫 B \cap Fin) ⋃_{y \in v} (y ball (D) r) = B$
175		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)$
176	26 174 175	sylanbrc	$⊢ φ \to D \in TotBnd (B)$

Metamath Proof Explorer

Theorem prdstotbnd

Proof