isbnd2

Description: The predicate "is a bounded metric space". Uses a single point instead of an arbitrary point in the space. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	isbnd2	$⊢ (M \in Bnd (X) \land X \neq \emptyset) \leftrightarrow (M \in ∞Met (X) \land \exists x \in X \exists r \in ℝ^{+} X = x ball (M) r)$

Proof

Step	Hyp	Ref	Expression
1		isbndx	$⊢ M \in Bnd (X) \leftrightarrow (M \in ∞Met (X) \land \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r)$
2	1	anbi1i	$⊢ (M \in Bnd (X) \land X \neq \emptyset) \leftrightarrow ((M \in ∞Met (X) \land \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r) \land X \neq \emptyset)$
3		anass	$⊢ ((M \in ∞Met (X) \land \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r) \land X \neq \emptyset) \leftrightarrow (M \in ∞Met (X) \land (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \land X \neq \emptyset))$
4		r19.2z	$⊢ (X \neq \emptyset \land \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r) \to \exists x \in X \exists r \in ℝ^{+} X = x ball (M) r$
5	4	ancoms	$⊢ (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \land X \neq \emptyset) \to \exists x \in X \exists r \in ℝ^{+} X = x ball (M) r$
6		oveq1	$⊢ x = y \to x ball (M) r = y ball (M) r$
7	6	eqeq2d	$⊢ x = y \to (X = x ball (M) r \leftrightarrow X = y ball (M) r)$
8		oveq2	$⊢ r = s \to y ball (M) r = y ball (M) s$
9	8	eqeq2d	$⊢ r = s \to (X = y ball (M) r \leftrightarrow X = y ball (M) s)$
10	7 9	cbvrex2vw	$⊢ \exists x \in X \exists r \in ℝ^{+} X = x ball (M) r \leftrightarrow \exists y \in X \exists s \in ℝ^{+} X = y ball (M) s$
11		2rp	$⊢ 2 \in ℝ^{+}$
12		rpmulcl	$⊢ (2 \in ℝ^{+} \land s \in ℝ^{+}) \to 2 s \in ℝ^{+}$
13	11 12	mpan	$⊢ s \in ℝ^{+} \to 2 s \in ℝ^{+}$
14	13	ad2antll	$⊢ (M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \to 2 s \in ℝ^{+}$
15	14	ad2antrr	$⊢ (((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land x \in X) \land X = y ball (M) s) \to 2 s \in ℝ^{+}$
16		rpcn	$⊢ s \in ℝ^{+} \to s \in ℂ$
17		2cnd	$⊢ s \in ℝ^{+} \to 2 \in ℂ$
18		2ne0	$⊢ 2 \neq 0$
19	18	a1i	$⊢ s \in ℝ^{+} \to 2 \neq 0$
20		divcan3	$⊢ (s \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{2 s}{2} = s$
21	20	eqcomd	$⊢ (s \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to s = \frac{2 s}{2}$
22	16 17 19 21	syl3anc	$⊢ s \in ℝ^{+} \to s = \frac{2 s}{2}$
23	22	oveq2d	$⊢ s \in ℝ^{+} \to y ball (M) s = y ball (M) (\frac{2 s}{2})$
24	23	eqeq2d	$⊢ s \in ℝ^{+} \to (X = y ball (M) s \leftrightarrow X = y ball (M) (\frac{2 s}{2}))$
25	24	biimpd	$⊢ s \in ℝ^{+} \to (X = y ball (M) s \to X = y ball (M) (\frac{2 s}{2}))$
26	25	ad2antll	$⊢ (M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \to (X = y ball (M) s \to X = y ball (M) (\frac{2 s}{2}))$
27	26	adantr	$⊢ ((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land x \in X) \to (X = y ball (M) s \to X = y ball (M) (\frac{2 s}{2}))$
28	27	imp	$⊢ (((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land x \in X) \land X = y ball (M) s) \to X = y ball (M) (\frac{2 s}{2})$
29		simpr	$⊢ (((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land x \in X) \land X = y ball (M) (\frac{2 s}{2})) \to X = y ball (M) (\frac{2 s}{2})$
30		eleq2	$⊢ X = y ball (M) (\frac{2 s}{2}) \to (x \in X \leftrightarrow x \in (y ball (M) (\frac{2 s}{2})))$
31	30	biimpac	$⊢ (x \in X \land X = y ball (M) (\frac{2 s}{2})) \to x \in (y ball (M) (\frac{2 s}{2}))$
32		2re	$⊢ 2 \in ℝ$
33		rpre	$⊢ s \in ℝ^{+} \to s \in ℝ$
34		remulcl	$⊢ (2 \in ℝ \land s \in ℝ) \to 2 s \in ℝ$
35	32 33 34	sylancr	$⊢ s \in ℝ^{+} \to 2 s \in ℝ$
36		blhalf	$⊢ ((M \in ∞Met (X) \land y \in X) \land (2 s \in ℝ \land x \in (y ball (M) (\frac{2 s}{2})))) \to y ball (M) (\frac{2 s}{2}) \subseteq x ball (M) 2 s$
37	36	expr	$⊢ ((M \in ∞Met (X) \land y \in X) \land 2 s \in ℝ) \to (x \in (y ball (M) (\frac{2 s}{2})) \to y ball (M) (\frac{2 s}{2}) \subseteq x ball (M) 2 s)$
38	35 37	sylan2	$⊢ ((M \in ∞Met (X) \land y \in X) \land s \in ℝ^{+}) \to (x \in (y ball (M) (\frac{2 s}{2})) \to y ball (M) (\frac{2 s}{2}) \subseteq x ball (M) 2 s)$
39	38	anasss	$⊢ (M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \to (x \in (y ball (M) (\frac{2 s}{2})) \to y ball (M) (\frac{2 s}{2}) \subseteq x ball (M) 2 s)$
40	39	imp	$⊢ ((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land x \in (y ball (M) (\frac{2 s}{2}))) \to y ball (M) (\frac{2 s}{2}) \subseteq x ball (M) 2 s$
41	31 40	sylan2	$⊢ ((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land (x \in X \land X = y ball (M) (\frac{2 s}{2}))) \to y ball (M) (\frac{2 s}{2}) \subseteq x ball (M) 2 s$
42	41	anassrs	$⊢ (((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land x \in X) \land X = y ball (M) (\frac{2 s}{2})) \to y ball (M) (\frac{2 s}{2}) \subseteq x ball (M) 2 s$
43	29 42	eqsstrd	$⊢ (((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land x \in X) \land X = y ball (M) (\frac{2 s}{2})) \to X \subseteq x ball (M) 2 s$
44	28 43	syldan	$⊢ (((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land x \in X) \land X = y ball (M) s) \to X \subseteq x ball (M) 2 s$
45	13	adantl	$⊢ (y \in X \land s \in ℝ^{+}) \to 2 s \in ℝ^{+}$
46		rpxr	$⊢ 2 s \in ℝ^{+} \to 2 s \in ℝ^{*}$
47		blssm	$⊢ (M \in ∞Met (X) \land x \in X \land 2 s \in ℝ^{*}) \to x ball (M) 2 s \subseteq X$
48	46 47	syl3an3	$⊢ (M \in ∞Met (X) \land x \in X \land 2 s \in ℝ^{+}) \to x ball (M) 2 s \subseteq X$
49	48	3expa	$⊢ ((M \in ∞Met (X) \land x \in X) \land 2 s \in ℝ^{+}) \to x ball (M) 2 s \subseteq X$
50	45 49	sylan2	$⊢ ((M \in ∞Met (X) \land x \in X) \land (y \in X \land s \in ℝ^{+})) \to x ball (M) 2 s \subseteq X$
51	50	an32s	$⊢ ((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land x \in X) \to x ball (M) 2 s \subseteq X$
52	51	adantr	$⊢ (((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land x \in X) \land X = y ball (M) s) \to x ball (M) 2 s \subseteq X$
53	44 52	eqssd	$⊢ (((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land x \in X) \land X = y ball (M) s) \to X = x ball (M) 2 s$
54		oveq2	$⊢ r = 2 s \to x ball (M) r = x ball (M) 2 s$
55	54	rspceeqv	$⊢ (2 s \in ℝ^{+} \land X = x ball (M) 2 s) \to \exists r \in ℝ^{+} X = x ball (M) r$
56	15 53 55	syl2anc	$⊢ (((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land x \in X) \land X = y ball (M) s) \to \exists r \in ℝ^{+} X = x ball (M) r$
57	56	ex	$⊢ ((M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \land x \in X) \to (X = y ball (M) s \to \exists r \in ℝ^{+} X = x ball (M) r)$
58	57	ralrimdva	$⊢ (M \in ∞Met (X) \land (y \in X \land s \in ℝ^{+})) \to (X = y ball (M) s \to \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r)$
59	58	rexlimdvva	$⊢ M \in ∞Met (X) \to (\exists y \in X \exists s \in ℝ^{+} X = y ball (M) s \to \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r)$
60	10 59	syl5bi	$⊢ M \in ∞Met (X) \to (\exists x \in X \exists r \in ℝ^{+} X = x ball (M) r \to \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r)$
61		rexn0	$⊢ \exists x \in X \exists r \in ℝ^{+} X = x ball (M) r \to X \neq \emptyset$
62	61	a1i	$⊢ M \in ∞Met (X) \to (\exists x \in X \exists r \in ℝ^{+} X = x ball (M) r \to X \neq \emptyset)$
63	60 62	jcad	$⊢ M \in ∞Met (X) \to (\exists x \in X \exists r \in ℝ^{+} X = x ball (M) r \to (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \land X \neq \emptyset))$
64	5 63	impbid2	$⊢ M \in ∞Met (X) \to ((\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \land X \neq \emptyset) \leftrightarrow \exists x \in X \exists r \in ℝ^{+} X = x ball (M) r)$
65	64	pm5.32i	$⊢ (M \in ∞Met (X) \land (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \land X \neq \emptyset)) \leftrightarrow (M \in ∞Met (X) \land \exists x \in X \exists r \in ℝ^{+} X = x ball (M) r)$
66	2 3 65	3bitri	$⊢ (M \in Bnd (X) \land X \neq \emptyset) \leftrightarrow (M \in ∞Met (X) \land \exists x \in X \exists r \in ℝ^{+} X = x ball (M) r)$

Metamath Proof Explorer

Theorem isbnd2

Proof