ssbnd

Description: A subset of a metric space is bounded iff it is contained in a ball around P , for any P in the larger space. (Contributed by Mario Carneiro, 14-Sep-2015)

		Ref	Expression
	Hypothesis	ssbnd.2	$⊢ N = {M ↾}_{(Y \times Y)}$
	Assertion	ssbnd	$⊢ (M \in Met (X) \land P \in X) \to (N \in Bnd (Y) \leftrightarrow \exists d \in ℝ Y \subseteq P ball (M) d)$

Proof

Step	Hyp	Ref	Expression
1		ssbnd.2	$⊢ N = {M ↾}_{(Y \times Y)}$
2		0re	$⊢ 0 \in ℝ$
3	2	ne0ii	$⊢ ℝ \neq \emptyset$
4		0ss	$⊢ \emptyset \subseteq P ball (M) d$
5		sseq1	$⊢ Y = \emptyset \to (Y \subseteq P ball (M) d \leftrightarrow \emptyset \subseteq P ball (M) d)$
6	4 5	mpbiri	$⊢ Y = \emptyset \to Y \subseteq P ball (M) d$
7	6	ralrimivw	$⊢ Y = \emptyset \to \forall d \in ℝ Y \subseteq P ball (M) d$
8		r19.2z	$⊢ (ℝ \neq \emptyset \land \forall d \in ℝ Y \subseteq P ball (M) d) \to \exists d \in ℝ Y \subseteq P ball (M) d$
9	3 7 8	sylancr	$⊢ Y = \emptyset \to \exists d \in ℝ Y \subseteq P ball (M) d$
10	9	a1i	$⊢ ((M \in Met (X) \land P \in X) \land N \in Bnd (Y)) \to (Y = \emptyset \to \exists d \in ℝ Y \subseteq P ball (M) d)$
11		isbnd2	$⊢ (N \in Bnd (Y) \land Y \neq \emptyset) \leftrightarrow (N \in ∞Met (Y) \land \exists y \in Y \exists r \in ℝ^{+} Y = y ball (N) r)$
12		simplll	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to M \in Met (X)$
13	1	dmeqi	$⊢ dom N = dom ({M ↾}_{(Y \times Y)})$
14		dmres	$⊢ dom ({M ↾}_{(Y \times Y)}) = (Y \times Y) \cap dom M$
15	13 14	eqtri	$⊢ dom N = (Y \times Y) \cap dom M$
16		xmetf	$⊢ N \in ∞Met (Y) \to N : Y \times Y ⟶ ℝ^{*}$
17	16	fdmd	$⊢ N \in ∞Met (Y) \to dom N = Y \times Y$
18	15 17	eqtr3id	$⊢ N \in ∞Met (Y) \to (Y \times Y) \cap dom M = Y \times Y$
19		df-ss	$⊢ Y \times Y \subseteq dom M \leftrightarrow (Y \times Y) \cap dom M = Y \times Y$
20	18 19	sylibr	$⊢ N \in ∞Met (Y) \to Y \times Y \subseteq dom M$
21	20	ad2antlr	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to Y \times Y \subseteq dom M$
22		metf	$⊢ M \in Met (X) \to M : X \times X ⟶ ℝ$
23	22	fdmd	$⊢ M \in Met (X) \to dom M = X \times X$
24	23	ad3antrrr	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to dom M = X \times X$
25	21 24	sseqtrd	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to Y \times Y \subseteq X \times X$
26		dmss	$⊢ Y \times Y \subseteq X \times X \to dom (Y \times Y) \subseteq dom (X \times X)$
27	25 26	syl	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to dom (Y \times Y) \subseteq dom (X \times X)$
28		dmxpid	$⊢ dom (Y \times Y) = Y$
29		dmxpid	$⊢ dom (X \times X) = X$
30	27 28 29	3sstr3g	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to Y \subseteq X$
31		simprl	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to y \in Y$
32	30 31	sseldd	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to y \in X$
33		simpllr	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to P \in X$
34		metcl	$⊢ (M \in Met (X) \land y \in X \land P \in X) \to y M P \in ℝ$
35	12 32 33 34	syl3anc	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to y M P \in ℝ$
36		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
37	36	ad2antll	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to r \in ℝ$
38	35 37	readdcld	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to (y M P) + r \in ℝ$
39		metxmet	$⊢ M \in Met (X) \to M \in ∞Met (X)$
40	12 39	syl	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to M \in ∞Met (X)$
41	32 31	elind	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to y \in (X \cap Y)$
42		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
43	42	ad2antll	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to r \in ℝ^{*}$
44	1	blres	$⊢ (M \in ∞Met (X) \land y \in (X \cap Y) \land r \in ℝ^{*}) \to y ball (N) r = (y ball (M) r) \cap Y$
45	40 41 43 44	syl3anc	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to y ball (N) r = (y ball (M) r) \cap Y$
46		inss1	$⊢ (y ball (M) r) \cap Y \subseteq y ball (M) r$
47	35	leidd	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to y M P \leq y M P$
48	35	recnd	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to y M P \in ℂ$
49	37	recnd	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to r \in ℂ$
50	48 49	pncand	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to (y M P) + r - r = y M P$
51	47 50	breqtrrd	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to y M P \leq (y M P) + r - r$
52		blss2	$⊢ ((M \in ∞Met (X) \land y \in X \land P \in X) \land (r \in ℝ \land (y M P) + r \in ℝ \land y M P \leq (y M P) + r - r)) \to y ball (M) r \subseteq P ball (M) ((y M P) + r)$
53	40 32 33 37 38 51 52	syl33anc	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to y ball (M) r \subseteq P ball (M) ((y M P) + r)$
54	46 53	sstrid	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to (y ball (M) r) \cap Y \subseteq P ball (M) ((y M P) + r)$
55	45 54	eqsstrd	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to y ball (N) r \subseteq P ball (M) ((y M P) + r)$
56		oveq2	$⊢ d = (y M P) + r \to P ball (M) d = P ball (M) ((y M P) + r)$
57	56	sseq2d	$⊢ d = (y M P) + r \to (y ball (N) r \subseteq P ball (M) d \leftrightarrow y ball (N) r \subseteq P ball (M) ((y M P) + r))$
58	57	rspcev	$⊢ ((y M P) + r \in ℝ \land y ball (N) r \subseteq P ball (M) ((y M P) + r)) \to \exists d \in ℝ y ball (N) r \subseteq P ball (M) d$
59	38 55 58	syl2anc	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to \exists d \in ℝ y ball (N) r \subseteq P ball (M) d$
60		sseq1	$⊢ Y = y ball (N) r \to (Y \subseteq P ball (M) d \leftrightarrow y ball (N) r \subseteq P ball (M) d)$
61	60	rexbidv	$⊢ Y = y ball (N) r \to (\exists d \in ℝ Y \subseteq P ball (M) d \leftrightarrow \exists d \in ℝ y ball (N) r \subseteq P ball (M) d)$
62	59 61	syl5ibrcom	$⊢ (((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \land (y \in Y \land r \in ℝ^{+})) \to (Y = y ball (N) r \to \exists d \in ℝ Y \subseteq P ball (M) d)$
63	62	rexlimdvva	$⊢ ((M \in Met (X) \land P \in X) \land N \in ∞Met (Y)) \to (\exists y \in Y \exists r \in ℝ^{+} Y = y ball (N) r \to \exists d \in ℝ Y \subseteq P ball (M) d)$
64	63	expimpd	$⊢ (M \in Met (X) \land P \in X) \to ((N \in ∞Met (Y) \land \exists y \in Y \exists r \in ℝ^{+} Y = y ball (N) r) \to \exists d \in ℝ Y \subseteq P ball (M) d)$
65	11 64	syl5bi	$⊢ (M \in Met (X) \land P \in X) \to ((N \in Bnd (Y) \land Y \neq \emptyset) \to \exists d \in ℝ Y \subseteq P ball (M) d)$
66	65	expdimp	$⊢ ((M \in Met (X) \land P \in X) \land N \in Bnd (Y)) \to (Y \neq \emptyset \to \exists d \in ℝ Y \subseteq P ball (M) d)$
67	10 66	pm2.61dne	$⊢ ((M \in Met (X) \land P \in X) \land N \in Bnd (Y)) \to \exists d \in ℝ Y \subseteq P ball (M) d$
68	67	ex	$⊢ (M \in Met (X) \land P \in X) \to (N \in Bnd (Y) \to \exists d \in ℝ Y \subseteq P ball (M) d)$
69		simprr	$⊢ ((M \in Met (X) \land P \in X) \land (d \in ℝ \land Y \subseteq P ball (M) d)) \to Y \subseteq P ball (M) d$
70		xpss12	$⊢ (Y \subseteq P ball (M) d \land Y \subseteq P ball (M) d) \to Y \times Y \subseteq (P ball (M) d) \times (P ball (M) d)$
71	69 69 70	syl2anc	$⊢ ((M \in Met (X) \land P \in X) \land (d \in ℝ \land Y \subseteq P ball (M) d)) \to Y \times Y \subseteq (P ball (M) d) \times (P ball (M) d)$
72	71	resabs1d	$⊢ ((M \in Met (X) \land P \in X) \land (d \in ℝ \land Y \subseteq P ball (M) d)) \to {({M ↾}_{((P ball (M) d) \times (P ball (M) d))}) ↾}_{(Y \times Y)} = {M ↾}_{(Y \times Y)}$
73	72 1	eqtr4di	$⊢ ((M \in Met (X) \land P \in X) \land (d \in ℝ \land Y \subseteq P ball (M) d)) \to {({M ↾}_{((P ball (M) d) \times (P ball (M) d))}) ↾}_{(Y \times Y)} = N$
74		blbnd	$⊢ (M \in ∞Met (X) \land P \in X \land d \in ℝ) \to {M ↾}_{((P ball (M) d) \times (P ball (M) d))} \in Bnd (P ball (M) d)$
75	39 74	syl3an1	$⊢ (M \in Met (X) \land P \in X \land d \in ℝ) \to {M ↾}_{((P ball (M) d) \times (P ball (M) d))} \in Bnd (P ball (M) d)$
76	75	3expa	$⊢ ((M \in Met (X) \land P \in X) \land d \in ℝ) \to {M ↾}_{((P ball (M) d) \times (P ball (M) d))} \in Bnd (P ball (M) d)$
77	76	adantrr	$⊢ ((M \in Met (X) \land P \in X) \land (d \in ℝ \land Y \subseteq P ball (M) d)) \to {M ↾}_{((P ball (M) d) \times (P ball (M) d))} \in Bnd (P ball (M) d)$
78		bndss	$⊢ ({M ↾}_{((P ball (M) d) \times (P ball (M) d))} \in Bnd (P ball (M) d) \land Y \subseteq P ball (M) d) \to {({M ↾}_{((P ball (M) d) \times (P ball (M) d))}) ↾}_{(Y \times Y)} \in Bnd (Y)$
79	77 69 78	syl2anc	$⊢ ((M \in Met (X) \land P \in X) \land (d \in ℝ \land Y \subseteq P ball (M) d)) \to {({M ↾}_{((P ball (M) d) \times (P ball (M) d))}) ↾}_{(Y \times Y)} \in Bnd (Y)$
80	73 79	eqeltrrd	$⊢ ((M \in Met (X) \land P \in X) \land (d \in ℝ \land Y \subseteq P ball (M) d)) \to N \in Bnd (Y)$
81	80	rexlimdvaa	$⊢ (M \in Met (X) \land P \in X) \to (\exists d \in ℝ Y \subseteq P ball (M) d \to N \in Bnd (Y))$
82	68 81	impbid	$⊢ (M \in Met (X) \land P \in X) \to (N \in Bnd (Y) \leftrightarrow \exists d \in ℝ Y \subseteq P ball (M) d)$

Metamath Proof Explorer

Theorem ssbnd

Proof