prdsbnd2

Description: If balls are totally bounded in each factor, then balls are bounded in a metric product. (Contributed by Mario Carneiro, 16-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$
	prdsbnd2.c	$⊢ C = {D ↾}_{(A \times A)}$
	prdsbnd2.e	$⊢ (φ \land x \in I) \to E \in Met (V)$
	prdsbnd2.m	$⊢ (φ \land x \in I) \to ({E ↾}_{(y \times y)} \in TotBnd (y) \leftrightarrow {E ↾}_{(y \times y)} \in Bnd (y))$
Assertion	prdsbnd2	$⊢ φ \to (C \in TotBnd (A) \leftrightarrow C \in Bnd (A))$

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		prdsbnd2.c	$⊢ C = {D ↾}_{(A \times A)}$
10		prdsbnd2.e	$⊢ (φ \land x \in I) \to E \in Met (V)$
11		prdsbnd2.m	$⊢ (φ \land x \in I) \to ({E ↾}_{(y \times y)} \in TotBnd (y) \leftrightarrow {E ↾}_{(y \times y)} \in Bnd (y))$
12		totbndbnd	$⊢ C \in TotBnd (A) \to C \in Bnd (A)$
13		bndmet	$⊢ C \in Bnd (A) \to C \in Met (A)$
14		0totbnd	$⊢ A = \emptyset \to (C \in TotBnd (A) \leftrightarrow C \in Met (A))$
15	13 14	imbitrrid	$⊢ A = \emptyset \to (C \in Bnd (A) \to C \in TotBnd (A))$
16	15	a1i	$⊢ φ \to (A = \emptyset \to (C \in Bnd (A) \to C \in TotBnd (A)))$
17		n0	$⊢ A \neq \emptyset \leftrightarrow \exists a a \in A$
18		simprr	$⊢ (φ \land (a \in A \land C \in Bnd (A))) \to C \in Bnd (A)$
19		eqid	$⊢ S ⨉_{𝑠} (x \in I ⟼ R (x)) = S ⨉_{𝑠} (x \in I ⟼ R (x))$
20		eqid	$⊢ {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))} = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
21		eqid	$⊢ dist (S ⨉_{𝑠} (x \in I ⟼ R (x))) = dist (S ⨉_{𝑠} (x \in I ⟼ R (x)))$
22		fvexd	$⊢ (φ \land x \in I) \to R (x) \in V$
23	19 20 3 4 21 6 7 22 10	prdsmet	$⊢ φ \to dist (S ⨉_{𝑠} (x \in I ⟼ R (x))) \in Met ({Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))})$
24		dffn5	$⊢ R Fn I \leftrightarrow R = (x \in I ⟼ R (x))$
25	8 24	sylib	$⊢ φ \to R = (x \in I ⟼ R (x))$
26	25	oveq2d	$⊢ φ \to S ⨉_{𝑠} R = S ⨉_{𝑠} (x \in I ⟼ R (x))$
27	1 26	eqtrid	$⊢ φ \to Y = S ⨉_{𝑠} (x \in I ⟼ R (x))$
28	27	fveq2d	$⊢ φ \to dist (Y) = dist (S ⨉_{𝑠} (x \in I ⟼ R (x)))$
29	5 28	eqtrid	$⊢ φ \to D = dist (S ⨉_{𝑠} (x \in I ⟼ R (x)))$
30	27	fveq2d	$⊢ φ \to {Base}_{Y} = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
31	2 30	eqtrid	$⊢ φ \to B = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
32	31	fveq2d	$⊢ φ \to Met (B) = Met ({Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))})$
33	23 29 32	3eltr4d	$⊢ φ \to D \in Met (B)$
34	33	adantr	$⊢ (φ \land (a \in A \land C \in Bnd (A))) \to D \in Met (B)$
35		simpr	$⊢ (a \in A \land C \in Bnd (A)) \to C \in Bnd (A)$
36	9	bnd2lem	$⊢ (D \in Met (B) \land C \in Bnd (A)) \to A \subseteq B$
37	33 35 36	syl2an	$⊢ (φ \land (a \in A \land C \in Bnd (A))) \to A \subseteq B$
38		simprl	$⊢ (φ \land (a \in A \land C \in Bnd (A))) \to a \in A$
39	37 38	sseldd	$⊢ (φ \land (a \in A \land C \in Bnd (A))) \to a \in B$
40	9	ssbnd	$⊢ (D \in Met (B) \land a \in B) \to (C \in Bnd (A) \leftrightarrow \exists r \in ℝ A \subseteq a ball (D) r)$
41	34 39 40	syl2anc	$⊢ (φ \land (a \in A \land C \in Bnd (A))) \to (C \in Bnd (A) \leftrightarrow \exists r \in ℝ A \subseteq a ball (D) r)$
42	18 41	mpbid	$⊢ (φ \land (a \in A \land C \in Bnd (A))) \to \exists r \in ℝ A \subseteq a ball (D) r$
43		simprr	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to A \subseteq a ball (D) r$
44		xpss12	$⊢ (A \subseteq a ball (D) r \land A \subseteq a ball (D) r) \to A \times A \subseteq (a ball (D) r) \times (a ball (D) r)$
45	43 43 44	syl2anc	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to A \times A \subseteq (a ball (D) r) \times (a ball (D) r)$
46	45	resabs1d	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to {({D ↾}_{((a ball (D) r) \times (a ball (D) r))}) ↾}_{(A \times A)} = {D ↾}_{(A \times A)}$
47	46 9	eqtr4di	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to {({D ↾}_{((a ball (D) r) \times (a ball (D) r))}) ↾}_{(A \times A)} = C$
48		simpll	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to φ$
49	39	adantr	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to a \in B$
50		simprl	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to r \in ℝ$
51	38	adantr	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to a \in A$
52	43 51	sseldd	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to a \in (a ball (D) r)$
53	52	ne0d	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to a ball (D) r \neq \emptyset$
54	33	ad2antrr	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to D \in Met (B)$
55		metxmet	$⊢ D \in Met (B) \to D \in ∞Met (B)$
56	54 55	syl	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to D \in ∞Met (B)$
57	50	rexrd	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to r \in ℝ^{*}$
58		xbln0	$⊢ (D \in ∞Met (B) \land a \in B \land r \in ℝ^{*}) \to (a ball (D) r \neq \emptyset \leftrightarrow 0 < r)$
59	56 49 57 58	syl3anc	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to (a ball (D) r \neq \emptyset \leftrightarrow 0 < r)$
60	53 59	mpbid	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to 0 < r$
61	50 60	elrpd	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to r \in ℝ^{+}$
62		eqid	$⊢ S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) = S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r))$
63		eqid	$⊢ {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)))} = {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)))}$
64		eqid	$⊢ {Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)} = {Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)}$
65		eqid	$⊢ {dist ((y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)) ↾}_{({Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)} \times {Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)})} = {dist ((y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)) ↾}_{({Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)} \times {Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)})}$
66		eqid	$⊢ dist (S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r))) = dist (S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)))$
67	6	adantr	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to S \in W$
68	7	adantr	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to I \in Fin$
69		ovex	$⊢ R (x) ↾_{𝑠} (a (x) ball (E) r) \in V$
70		fveq2	$⊢ y = x \to R (y) = R (x)$
71		2fveq3	$⊢ y = x \to dist (R (y)) = dist (R (x))$
72		2fveq3	$⊢ y = x \to {Base}_{R (y)} = {Base}_{R (x)}$
73	72 3	eqtr4di	$⊢ y = x \to {Base}_{R (y)} = V$
74	73	sqxpeqd	$⊢ y = x \to {Base}_{R (y)} \times {Base}_{R (y)} = V \times V$
75	71 74	reseq12d	$⊢ y = x \to {dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})} = {dist (R (x)) ↾}_{(V \times V)}$
76	75 4	eqtr4di	$⊢ y = x \to {dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})} = E$
77	76	fveq2d	$⊢ y = x \to ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) = ball (E)$
78		fveq2	$⊢ y = x \to a (y) = a (x)$
79		eqidd	$⊢ y = x \to r = r$
80	77 78 79	oveq123d	$⊢ y = x \to a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r = a (x) ball (E) r$
81	70 80	oveq12d	$⊢ y = x \to R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r) = R (x) ↾_{𝑠} (a (x) ball (E) r)$
82	81	cbvmptv	$⊢ (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) = (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r))$
83	69 82	fnmpti	$⊢ (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) Fn I$
84	83	a1i	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) Fn I$
85	10	adantlr	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to E \in Met (V)$
86		metxmet	$⊢ E \in Met (V) \to E \in ∞Met (V)$
87	85 86	syl	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to E \in ∞Met (V)$
88	22	ralrimiva	$⊢ φ \to \forall x \in I R (x) \in V$
89	88	adantr	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to \forall x \in I R (x) \in V$
90		simprl	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to a \in B$
91	31	adantr	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to B = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
92	90 91	eleqtrd	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to a \in {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x)))}$
93	19 20 67 68 89 3 92	prdsbascl	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to \forall x \in I a (x) \in V$
94	93	r19.21bi	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to a (x) \in V$
95		simplrr	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to r \in ℝ^{+}$
96	95	rpred	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to r \in ℝ$
97		blbnd	$⊢ (E \in ∞Met (V) \land a (x) \in V \land r \in ℝ) \to {E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} \in Bnd (a (x) ball (E) r)$
98	87 94 96 97	syl3anc	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to {E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} \in Bnd (a (x) ball (E) r)$
99		ovex	$⊢ a (x) ball (E) r \in V$
100		xpeq12	$⊢ (y = a (x) ball (E) r \land y = a (x) ball (E) r) \to y \times y = (a (x) ball (E) r) \times (a (x) ball (E) r)$
101	100	anidms	$⊢ y = a (x) ball (E) r \to y \times y = (a (x) ball (E) r) \times (a (x) ball (E) r)$
102	101	reseq2d	$⊢ y = a (x) ball (E) r \to {E ↾}_{(y \times y)} = {E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))}$
103		fveq2	$⊢ y = a (x) ball (E) r \to TotBnd (y) = TotBnd (a (x) ball (E) r)$
104	102 103	eleq12d	$⊢ y = a (x) ball (E) r \to ({E ↾}_{(y \times y)} \in TotBnd (y) \leftrightarrow {E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} \in TotBnd (a (x) ball (E) r))$
105		fveq2	$⊢ y = a (x) ball (E) r \to Bnd (y) = Bnd (a (x) ball (E) r)$
106	102 105	eleq12d	$⊢ y = a (x) ball (E) r \to ({E ↾}_{(y \times y)} \in Bnd (y) \leftrightarrow {E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} \in Bnd (a (x) ball (E) r))$
107	104 106	bibi12d	$⊢ y = a (x) ball (E) r \to (({E ↾}_{(y \times y)} \in TotBnd (y) \leftrightarrow {E ↾}_{(y \times y)} \in Bnd (y)) \leftrightarrow ({E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} \in TotBnd (a (x) ball (E) r) \leftrightarrow {E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} \in Bnd (a (x) ball (E) r)))$
108	107	imbi2d	$⊢ y = a (x) ball (E) r \to (((φ \land x \in I) \to ({E ↾}_{(y \times y)} \in TotBnd (y) \leftrightarrow {E ↾}_{(y \times y)} \in Bnd (y))) \leftrightarrow ((φ \land x \in I) \to ({E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} \in TotBnd (a (x) ball (E) r) \leftrightarrow {E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} \in Bnd (a (x) ball (E) r))))$
109	99 108 11	vtocl	$⊢ (φ \land x \in I) \to ({E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} \in TotBnd (a (x) ball (E) r) \leftrightarrow {E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} \in Bnd (a (x) ball (E) r))$
110	109	adantlr	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to ({E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} \in TotBnd (a (x) ball (E) r) \leftrightarrow {E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} \in Bnd (a (x) ball (E) r))$
111	98 110	mpbird	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to {E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} \in TotBnd (a (x) ball (E) r)$
112		eqid	$⊢ (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) = (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r))$
113	81 112 69	fvmpt	$⊢ x \in I \to (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x) = R (x) ↾_{𝑠} (a (x) ball (E) r)$
114	113	adantl	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x) = R (x) ↾_{𝑠} (a (x) ball (E) r)$
115	114	fveq2d	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to dist ((y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)) = dist (R (x) ↾_{𝑠} (a (x) ball (E) r))$
116		eqid	$⊢ R (x) ↾_{𝑠} (a (x) ball (E) r) = R (x) ↾_{𝑠} (a (x) ball (E) r)$
117		eqid	$⊢ dist (R (x)) = dist (R (x))$
118	116 117	ressds	$⊢ a (x) ball (E) r \in V \to dist (R (x)) = dist (R (x) ↾_{𝑠} (a (x) ball (E) r))$
119	99 118	ax-mp	$⊢ dist (R (x)) = dist (R (x) ↾_{𝑠} (a (x) ball (E) r))$
120	115 119	eqtr4di	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to dist ((y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)) = dist (R (x))$
121	114	fveq2d	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to {Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)} = {Base}_{(R (x) ↾_{𝑠} (a (x) ball (E) r))}$
122		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
123	122	ad2antll	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to r \in ℝ^{*}$
124	123	adantr	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to r \in ℝ^{*}$
125		blssm	$⊢ (E \in ∞Met (V) \land a (x) \in V \land r \in ℝ^{*}) \to a (x) ball (E) r \subseteq V$
126	87 94 124 125	syl3anc	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to a (x) ball (E) r \subseteq V$
127	116 3	ressbas2	$⊢ a (x) ball (E) r \subseteq V \to a (x) ball (E) r = {Base}_{(R (x) ↾_{𝑠} (a (x) ball (E) r))}$
128	126 127	syl	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to a (x) ball (E) r = {Base}_{(R (x) ↾_{𝑠} (a (x) ball (E) r))}$
129	121 128	eqtr4d	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to {Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)} = a (x) ball (E) r$
130	129	sqxpeqd	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to {Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)} \times {Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)} = (a (x) ball (E) r) \times (a (x) ball (E) r)$
131	120 130	reseq12d	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to {dist ((y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)) ↾}_{({Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)} \times {Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)})} = {dist (R (x)) ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))}$
132	4	reseq1i	$⊢ {E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} = {({dist (R (x)) ↾}_{(V \times V)}) ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))}$
133		xpss12	$⊢ (a (x) ball (E) r \subseteq V \land a (x) ball (E) r \subseteq V) \to (a (x) ball (E) r) \times (a (x) ball (E) r) \subseteq V \times V$
134	126 126 133	syl2anc	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to (a (x) ball (E) r) \times (a (x) ball (E) r) \subseteq V \times V$
135	134	resabs1d	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to {({dist (R (x)) ↾}_{(V \times V)}) ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} = {dist (R (x)) ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))}$
136	132 135	eqtrid	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to {E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))} = {dist (R (x)) ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))}$
137	131 136	eqtr4d	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to {dist ((y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)) ↾}_{({Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)} \times {Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)})} = {E ↾}_{((a (x) ball (E) r) \times (a (x) ball (E) r))}$
138	129	fveq2d	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to TotBnd ({Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)}) = TotBnd (a (x) ball (E) r)$
139	111 137 138	3eltr4d	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to {dist ((y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)) ↾}_{({Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)} \times {Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)})} \in TotBnd ({Base}_{(y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) (x)})$
140	62 63 64 65 66 67 68 84 139	prdstotbnd	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to dist (S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r))) \in TotBnd ({Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)))})$
141	27	adantr	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to Y = S ⨉_{𝑠} (x \in I ⟼ R (x))$
142		eqidd	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)) = S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r))$
143		eqid	$⊢ {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)))} = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)))}$
144	82	oveq2i	$⊢ S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)) = S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r))$
145	144	fveq2i	$⊢ dist (S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r))) = dist (S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)))$
146		fvexd	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to R (x) \in V$
147	99	a1i	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to a (x) ball (E) r \in V$
148	141 142 143 5 145 67 67 68 146 147	ressprdsds	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to dist (S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r))) = {D ↾}_{({Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)))} \times {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)))})}$
149	128	ixpeq2dva	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to \underset{x \in I}{⨉} (a (x) ball (E) r) = \underset{x \in I}{⨉} {Base}_{(R (x) ↾_{𝑠} (a (x) ball (E) r))}$
150	70	cbvmptv	$⊢ (y \in I ⟼ R (y)) = (x \in I ⟼ R (x))$
151	150	oveq2i	$⊢ S ⨉_{𝑠} (y \in I ⟼ R (y)) = S ⨉_{𝑠} (x \in I ⟼ R (x))$
152	27 151	eqtr4di	$⊢ φ \to Y = S ⨉_{𝑠} (y \in I ⟼ R (y))$
153	152	fveq2d	$⊢ φ \to dist (Y) = dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))$
154	5 153	eqtrid	$⊢ φ \to D = dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))$
155	154	fveq2d	$⊢ φ \to ball (D) = ball (dist (S ⨉_{𝑠} (y \in I ⟼ R (y))))$
156	155	oveqdr	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to a ball (D) r = a ball (dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))) r$
157		eqid	$⊢ {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))} = {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
158		eqid	$⊢ dist (S ⨉_{𝑠} (y \in I ⟼ R (y))) = dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))$
159	152	fveq2d	$⊢ φ \to {Base}_{Y} = {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
160	2 159	eqtrid	$⊢ φ \to B = {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
161	160	adantr	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to B = {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
162	90 161	eleqtrd	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to a \in {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y)))}$
163		rpgt0	$⊢ r \in ℝ^{+} \to 0 < r$
164	163	ad2antll	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to 0 < r$
165	151 157 3 4 158 67 68 146 87 162 123 164	prdsbl	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to a ball (dist (S ⨉_{𝑠} (y \in I ⟼ R (y)))) r = \underset{x \in I}{⨉} (a (x) ball (E) r)$
166	156 165	eqtrd	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to a ball (D) r = \underset{x \in I}{⨉} (a (x) ball (E) r)$
167		eqid	$⊢ S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)) = S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r))$
168	69	a1i	$⊢ ((φ \land (a \in B \land r \in ℝ^{+})) \land x \in I) \to R (x) ↾_{𝑠} (a (x) ball (E) r) \in V$
169	168	ralrimiva	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to \forall x \in I R (x) ↾_{𝑠} (a (x) ball (E) r) \in V$
170		eqid	$⊢ {Base}_{(R (x) ↾_{𝑠} (a (x) ball (E) r))} = {Base}_{(R (x) ↾_{𝑠} (a (x) ball (E) r))}$
171	167 143 67 68 169 170	prdsbas3	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)))} = \underset{x \in I}{⨉} {Base}_{(R (x) ↾_{𝑠} (a (x) ball (E) r))}$
172	149 166 171	3eqtr4rd	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)))} = a ball (D) r$
173	172	sqxpeqd	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)))} \times {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)))} = (a ball (D) r) \times (a ball (D) r)$
174	173	reseq2d	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to {D ↾}_{({Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)))} \times {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)))})} = {D ↾}_{((a ball (D) r) \times (a ball (D) r))}$
175	148 174	eqtrd	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to dist (S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r))) = {D ↾}_{((a ball (D) r) \times (a ball (D) r))}$
176	144	fveq2i	$⊢ {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)))} = {Base}_{(S ⨉_{𝑠} (x \in I ⟼ R (x) ↾_{𝑠} (a (x) ball (E) r)))}$
177	176 172	eqtrid	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to {Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)))} = a ball (D) r$
178	177	fveq2d	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to TotBnd ({Base}_{(S ⨉_{𝑠} (y \in I ⟼ R (y) ↾_{𝑠} (a (y) ball ({dist (R (y)) ↾}_{({Base}_{R (y)} \times {Base}_{R (y)})}) r)))}) = TotBnd (a ball (D) r)$
179	140 175 178	3eltr3d	$⊢ (φ \land (a \in B \land r \in ℝ^{+})) \to {D ↾}_{((a ball (D) r) \times (a ball (D) r))} \in TotBnd (a ball (D) r)$
180	48 49 61 179	syl12anc	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to {D ↾}_{((a ball (D) r) \times (a ball (D) r))} \in TotBnd (a ball (D) r)$
181		totbndss	$⊢ ({D ↾}_{((a ball (D) r) \times (a ball (D) r))} \in TotBnd (a ball (D) r) \land A \subseteq a ball (D) r) \to {({D ↾}_{((a ball (D) r) \times (a ball (D) r))}) ↾}_{(A \times A)} \in TotBnd (A)$
182	180 43 181	syl2anc	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to {({D ↾}_{((a ball (D) r) \times (a ball (D) r))}) ↾}_{(A \times A)} \in TotBnd (A)$
183	47 182	eqeltrrd	$⊢ ((φ \land (a \in A \land C \in Bnd (A))) \land (r \in ℝ \land A \subseteq a ball (D) r)) \to C \in TotBnd (A)$
184	42 183	rexlimddv	$⊢ (φ \land (a \in A \land C \in Bnd (A))) \to C \in TotBnd (A)$
185	184	exp32	$⊢ φ \to (a \in A \to (C \in Bnd (A) \to C \in TotBnd (A)))$
186	185	exlimdv	$⊢ φ \to (\exists a a \in A \to (C \in Bnd (A) \to C \in TotBnd (A)))$
187	17 186	biimtrid	$⊢ φ \to (A \neq \emptyset \to (C \in Bnd (A) \to C \in TotBnd (A)))$
188	16 187	pm2.61dne	$⊢ φ \to (C \in Bnd (A) \to C \in TotBnd (A))$
189	12 188	impbid2	$⊢ φ \to (C \in TotBnd (A) \leftrightarrow C \in Bnd (A))$

Metamath Proof Explorer

Theorem prdsbnd2

Proof