bndss

Description: A subset of a bounded metric space is bounded. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	bndss	$⊢ (M \in Bnd (X) \land S \subseteq X) \to {M ↾}_{(S \times S)} \in Bnd (S)$

Proof

Step	Hyp	Ref	Expression
1		metres2	$⊢ (M \in Met (X) \land S \subseteq X) \to {M ↾}_{(S \times S)} \in Met (S)$
2	1	adantlr	$⊢ ((M \in Met (X) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r) \land S \subseteq X) \to {M ↾}_{(S \times S)} \in Met (S)$
3		ssel2	$⊢ (S \subseteq X \land x \in S) \to x \in X$
4	3	ancoms	$⊢ (x \in S \land S \subseteq X) \to x \in X$
5		oveq1	$⊢ y = x \to y ball (M) r = x ball (M) r$
6	5	eqeq2d	$⊢ y = x \to (X = y ball (M) r \leftrightarrow X = x ball (M) r)$
7	6	rexbidv	$⊢ y = x \to (\exists r \in ℝ^{+} X = y ball (M) r \leftrightarrow \exists r \in ℝ^{+} X = x ball (M) r)$
8	7	rspcva	$⊢ (x \in X \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r) \to \exists r \in ℝ^{+} X = x ball (M) r$
9	4 8	sylan	$⊢ ((x \in S \land S \subseteq X) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r) \to \exists r \in ℝ^{+} X = x ball (M) r$
10	9	adantlll	$⊢ (((M \in Met (X) \land x \in S) \land S \subseteq X) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r) \to \exists r \in ℝ^{+} X = x ball (M) r$
11		dfss	$⊢ S \subseteq X \leftrightarrow S = S \cap X$
12	11	biimpi	$⊢ S \subseteq X \to S = S \cap X$
13		incom	$⊢ S \cap X = X \cap S$
14	12 13	eqtrdi	$⊢ S \subseteq X \to S = X \cap S$
15		ineq1	$⊢ X = x ball (M) r \to X \cap S = (x ball (M) r) \cap S$
16	14 15	sylan9eq	$⊢ (S \subseteq X \land X = x ball (M) r) \to S = (x ball (M) r) \cap S$
17	16	adantll	$⊢ (((M \in Met (X) \land x \in S) \land S \subseteq X) \land X = x ball (M) r) \to S = (x ball (M) r) \cap S$
18	17	adantlr	$⊢ ((((M \in Met (X) \land x \in S) \land S \subseteq X) \land r \in ℝ^{+}) \land X = x ball (M) r) \to S = (x ball (M) r) \cap S$
19		eqid	$⊢ {M ↾}_{(S \times S)} = {M ↾}_{(S \times S)}$
20	19	blssp	$⊢ ((M \in Met (X) \land S \subseteq X) \land (x \in S \land r \in ℝ^{+})) \to x ball ({M ↾}_{(S \times S)}) r = (x ball (M) r) \cap S$
21	20	an4s	$⊢ ((M \in Met (X) \land x \in S) \land (S \subseteq X \land r \in ℝ^{+})) \to x ball ({M ↾}_{(S \times S)}) r = (x ball (M) r) \cap S$
22	21	anassrs	$⊢ (((M \in Met (X) \land x \in S) \land S \subseteq X) \land r \in ℝ^{+}) \to x ball ({M ↾}_{(S \times S)}) r = (x ball (M) r) \cap S$
23	22	adantr	$⊢ ((((M \in Met (X) \land x \in S) \land S \subseteq X) \land r \in ℝ^{+}) \land X = x ball (M) r) \to x ball ({M ↾}_{(S \times S)}) r = (x ball (M) r) \cap S$
24	18 23	eqtr4d	$⊢ ((((M \in Met (X) \land x \in S) \land S \subseteq X) \land r \in ℝ^{+}) \land X = x ball (M) r) \to S = x ball ({M ↾}_{(S \times S)}) r$
25	24	ex	$⊢ (((M \in Met (X) \land x \in S) \land S \subseteq X) \land r \in ℝ^{+}) \to (X = x ball (M) r \to S = x ball ({M ↾}_{(S \times S)}) r)$
26	25	reximdva	$⊢ ((M \in Met (X) \land x \in S) \land S \subseteq X) \to (\exists r \in ℝ^{+} X = x ball (M) r \to \exists r \in ℝ^{+} S = x ball ({M ↾}_{(S \times S)}) r)$
27	26	imp	$⊢ (((M \in Met (X) \land x \in S) \land S \subseteq X) \land \exists r \in ℝ^{+} X = x ball (M) r) \to \exists r \in ℝ^{+} S = x ball ({M ↾}_{(S \times S)}) r$
28	10 27	syldan	$⊢ (((M \in Met (X) \land x \in S) \land S \subseteq X) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r) \to \exists r \in ℝ^{+} S = x ball ({M ↾}_{(S \times S)}) r$
29	28	an32s	$⊢ (((M \in Met (X) \land x \in S) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r) \land S \subseteq X) \to \exists r \in ℝ^{+} S = x ball ({M ↾}_{(S \times S)}) r$
30	29	ex	$⊢ ((M \in Met (X) \land x \in S) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r) \to (S \subseteq X \to \exists r \in ℝ^{+} S = x ball ({M ↾}_{(S \times S)}) r)$
31	30	an32s	$⊢ ((M \in Met (X) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r) \land x \in S) \to (S \subseteq X \to \exists r \in ℝ^{+} S = x ball ({M ↾}_{(S \times S)}) r)$
32	31	imp	$⊢ (((M \in Met (X) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r) \land x \in S) \land S \subseteq X) \to \exists r \in ℝ^{+} S = x ball ({M ↾}_{(S \times S)}) r$
33	32	an32s	$⊢ (((M \in Met (X) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r) \land S \subseteq X) \land x \in S) \to \exists r \in ℝ^{+} S = x ball ({M ↾}_{(S \times S)}) r$
34	33	ralrimiva	$⊢ ((M \in Met (X) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r) \land S \subseteq X) \to \forall x \in S \exists r \in ℝ^{+} S = x ball ({M ↾}_{(S \times S)}) r$
35	2 34	jca	$⊢ ((M \in Met (X) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r) \land S \subseteq X) \to ({M ↾}_{(S \times S)} \in Met (S) \land \forall x \in S \exists r \in ℝ^{+} S = x ball ({M ↾}_{(S \times S)}) r)$
36		isbnd	$⊢ M \in Bnd (X) \leftrightarrow (M \in Met (X) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r)$
37	36	anbi1i	$⊢ (M \in Bnd (X) \land S \subseteq X) \leftrightarrow ((M \in Met (X) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r) \land S \subseteq X)$
38		isbnd	$⊢ {M ↾}_{(S \times S)} \in Bnd (S) \leftrightarrow ({M ↾}_{(S \times S)} \in Met (S) \land \forall x \in S \exists r \in ℝ^{+} S = x ball ({M ↾}_{(S \times S)}) r)$
39	35 37 38	3imtr4i	$⊢ (M \in Bnd (X) \land S \subseteq X) \to {M ↾}_{(S \times S)} \in Bnd (S)$

Metamath Proof Explorer

Theorem bndss

Proof