isbnd3

Description: A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 13-Sep-2015)

		Ref	Expression
	Assertion	isbnd3	$⊢ M \in Bnd (X) \leftrightarrow (M \in Met (X) \land \exists x \in ℝ M : X \times X ⟶ [0, x])$

Proof

Step	Hyp	Ref	Expression
1		bndmet	$⊢ M \in Bnd (X) \to M \in Met (X)$
2		0re	$⊢ 0 \in ℝ$
3	2	ne0ii	$⊢ ℝ \neq \emptyset$
4		metf	$⊢ M \in Met (X) \to M : X \times X ⟶ ℝ$
5	4	ffnd	$⊢ M \in Met (X) \to M Fn (X \times X)$
6	1 5	syl	$⊢ M \in Bnd (X) \to M Fn (X \times X)$
7	6	ad2antrr	$⊢ ((M \in Bnd (X) \land X = \emptyset) \land x \in ℝ) \to M Fn (X \times X)$
8	1 4	syl	$⊢ M \in Bnd (X) \to M : X \times X ⟶ ℝ$
9	8	fdmd	$⊢ M \in Bnd (X) \to dom M = X \times X$
10		xpeq2	$⊢ X = \emptyset \to X \times X = X \times \emptyset$
11		xp0	$⊢ X \times \emptyset = \emptyset$
12	10 11	eqtrdi	$⊢ X = \emptyset \to X \times X = \emptyset$
13	9 12	sylan9eq	$⊢ (M \in Bnd (X) \land X = \emptyset) \to dom M = \emptyset$
14	13	adantr	$⊢ ((M \in Bnd (X) \land X = \emptyset) \land x \in ℝ) \to dom M = \emptyset$
15		dm0rn0	$⊢ dom M = \emptyset \leftrightarrow ran M = \emptyset$
16	14 15	sylib	$⊢ ((M \in Bnd (X) \land X = \emptyset) \land x \in ℝ) \to ran M = \emptyset$
17		0ss	$⊢ \emptyset \subseteq [0, x]$
18	16 17	eqsstrdi	$⊢ ((M \in Bnd (X) \land X = \emptyset) \land x \in ℝ) \to ran M \subseteq [0, x]$
19		df-f	$⊢ M : X \times X ⟶ [0, x] \leftrightarrow (M Fn (X \times X) \land ran M \subseteq [0, x])$
20	7 18 19	sylanbrc	$⊢ ((M \in Bnd (X) \land X = \emptyset) \land x \in ℝ) \to M : X \times X ⟶ [0, x]$
21	20	ralrimiva	$⊢ (M \in Bnd (X) \land X = \emptyset) \to \forall x \in ℝ M : X \times X ⟶ [0, x]$
22		r19.2z	$⊢ (ℝ \neq \emptyset \land \forall x \in ℝ M : X \times X ⟶ [0, x]) \to \exists x \in ℝ M : X \times X ⟶ [0, x]$
23	3 21 22	sylancr	$⊢ (M \in Bnd (X) \land X = \emptyset) \to \exists x \in ℝ M : X \times X ⟶ [0, x]$
24		isbnd2	$⊢ (M \in Bnd (X) \land X \neq \emptyset) \leftrightarrow (M \in ∞Met (X) \land \exists y \in X \exists r \in ℝ^{+} X = y ball (M) r)$
25	24	simprbi	$⊢ (M \in Bnd (X) \land X \neq \emptyset) \to \exists y \in X \exists r \in ℝ^{+} X = y ball (M) r$
26		2re	$⊢ 2 \in ℝ$
27		simprlr	$⊢ (M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \to r \in ℝ^{+}$
28	27	rpred	$⊢ (M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \to r \in ℝ$
29		remulcl	$⊢ (2 \in ℝ \land r \in ℝ) \to 2 r \in ℝ$
30	26 28 29	sylancr	$⊢ (M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \to 2 r \in ℝ$
31	5	adantr	$⊢ (M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \to M Fn (X \times X)$
32		simpll	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to M \in Met (X)$
33		simprl	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to x \in X$
34		simprr	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to z \in X$
35		metcl	$⊢ (M \in Met (X) \land x \in X \land z \in X) \to x M z \in ℝ$
36	32 33 34 35	syl3anc	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to x M z \in ℝ$
37		metge0	$⊢ (M \in Met (X) \land x \in X \land z \in X) \to 0 \leq x M z$
38	32 33 34 37	syl3anc	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to 0 \leq x M z$
39	30	adantr	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to 2 r \in ℝ$
40		simprll	$⊢ (M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \to y \in X$
41	40	adantr	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to y \in X$
42		metcl	$⊢ (M \in Met (X) \land y \in X \land x \in X) \to y M x \in ℝ$
43	32 41 33 42	syl3anc	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to y M x \in ℝ$
44		metcl	$⊢ (M \in Met (X) \land y \in X \land z \in X) \to y M z \in ℝ$
45	32 41 34 44	syl3anc	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to y M z \in ℝ$
46	43 45	readdcld	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to (y M x) + (y M z) \in ℝ$
47		mettri2	$⊢ (M \in Met (X) \land (y \in X \land x \in X \land z \in X)) \to x M z \leq (y M x) + (y M z)$
48	32 41 33 34 47	syl13anc	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to x M z \leq (y M x) + (y M z)$
49	28	adantr	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to r \in ℝ$
50		simplrr	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to X = y ball (M) r$
51	33 50	eleqtrd	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to x \in (y ball (M) r)$
52		metxmet	$⊢ M \in Met (X) \to M \in ∞Met (X)$
53	32 52	syl	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to M \in ∞Met (X)$
54		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
55	54	ad2antlr	$⊢ ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r) \to r \in ℝ^{*}$
56	55	ad2antlr	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to r \in ℝ^{*}$
57		elbl2	$⊢ ((M \in ∞Met (X) \land r \in ℝ^{*}) \land (y \in X \land x \in X)) \to (x \in (y ball (M) r) \leftrightarrow y M x < r)$
58	53 56 41 33 57	syl22anc	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to (x \in (y ball (M) r) \leftrightarrow y M x < r)$
59	51 58	mpbid	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to y M x < r$
60	34 50	eleqtrd	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to z \in (y ball (M) r)$
61		elbl2	$⊢ ((M \in ∞Met (X) \land r \in ℝ^{*}) \land (y \in X \land z \in X)) \to (z \in (y ball (M) r) \leftrightarrow y M z < r)$
62	53 56 41 34 61	syl22anc	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to (z \in (y ball (M) r) \leftrightarrow y M z < r)$
63	60 62	mpbid	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to y M z < r$
64	43 45 49 49 59 63	lt2addd	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to (y M x) + (y M z) < r + r$
65	49	recnd	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to r \in ℂ$
66	65	2timesd	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to 2 r = r + r$
67	64 66	breqtrrd	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to (y M x) + (y M z) < 2 r$
68	36 46 39 48 67	lelttrd	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to x M z < 2 r$
69	36 39 68	ltled	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to x M z \leq 2 r$
70		elicc2	$⊢ (0 \in ℝ \land 2 r \in ℝ) \to (x M z \in [0, 2 r] \leftrightarrow (x M z \in ℝ \land 0 \leq x M z \land x M z \leq 2 r))$
71	2 39 70	sylancr	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to (x M z \in [0, 2 r] \leftrightarrow (x M z \in ℝ \land 0 \leq x M z \land x M z \leq 2 r))$
72	36 38 69 71	mpbir3and	$⊢ ((M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \land (x \in X \land z \in X)) \to x M z \in [0, 2 r]$
73	72	ralrimivva	$⊢ (M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \to \forall x \in X \forall z \in X x M z \in [0, 2 r]$
74		ffnov	$⊢ M : X \times X ⟶ [0, 2 r] \leftrightarrow (M Fn (X \times X) \land \forall x \in X \forall z \in X x M z \in [0, 2 r])$
75	31 73 74	sylanbrc	$⊢ (M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \to M : X \times X ⟶ [0, 2 r]$
76		oveq2	$⊢ x = 2 r \to [0, x] = [0, 2 r]$
77	76	feq3d	$⊢ x = 2 r \to (M : X \times X ⟶ [0, x] \leftrightarrow M : X \times X ⟶ [0, 2 r])$
78	77	rspcev	$⊢ (2 r \in ℝ \land M : X \times X ⟶ [0, 2 r]) \to \exists x \in ℝ M : X \times X ⟶ [0, x]$
79	30 75 78	syl2anc	$⊢ (M \in Met (X) \land ((y \in X \land r \in ℝ^{+}) \land X = y ball (M) r)) \to \exists x \in ℝ M : X \times X ⟶ [0, x]$
80	79	expr	$⊢ (M \in Met (X) \land (y \in X \land r \in ℝ^{+})) \to (X = y ball (M) r \to \exists x \in ℝ M : X \times X ⟶ [0, x])$
81	80	rexlimdvva	$⊢ M \in Met (X) \to (\exists y \in X \exists r \in ℝ^{+} X = y ball (M) r \to \exists x \in ℝ M : X \times X ⟶ [0, x])$
82	1 81	syl	$⊢ M \in Bnd (X) \to (\exists y \in X \exists r \in ℝ^{+} X = y ball (M) r \to \exists x \in ℝ M : X \times X ⟶ [0, x])$
83	82	adantr	$⊢ (M \in Bnd (X) \land X \neq \emptyset) \to (\exists y \in X \exists r \in ℝ^{+} X = y ball (M) r \to \exists x \in ℝ M : X \times X ⟶ [0, x])$
84	25 83	mpd	$⊢ (M \in Bnd (X) \land X \neq \emptyset) \to \exists x \in ℝ M : X \times X ⟶ [0, x]$
85	23 84	pm2.61dane	$⊢ M \in Bnd (X) \to \exists x \in ℝ M : X \times X ⟶ [0, x]$
86	1 85	jca	$⊢ M \in Bnd (X) \to (M \in Met (X) \land \exists x \in ℝ M : X \times X ⟶ [0, x])$
87		simpll	$⊢ ((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \to M \in Met (X)$
88		simpllr	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to x \in ℝ$
89	87	adantr	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to M \in Met (X)$
90		simpr	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to y \in X$
91		met0	$⊢ (M \in Met (X) \land y \in X) \to y M y = 0$
92	89 90 91	syl2anc	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to y M y = 0$
93		simplr	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to M : X \times X ⟶ [0, x]$
94	93 90 90	fovcdmd	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to y M y \in [0, x]$
95		elicc2	$⊢ (0 \in ℝ \land x \in ℝ) \to (y M y \in [0, x] \leftrightarrow (y M y \in ℝ \land 0 \leq y M y \land y M y \leq x))$
96	2 88 95	sylancr	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to (y M y \in [0, x] \leftrightarrow (y M y \in ℝ \land 0 \leq y M y \land y M y \leq x))$
97	94 96	mpbid	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to (y M y \in ℝ \land 0 \leq y M y \land y M y \leq x)$
98	97	simp3d	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to y M y \leq x$
99	92 98	eqbrtrrd	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to 0 \leq x$
100	88 99	ge0p1rpd	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to x + 1 \in ℝ^{+}$
101		fovcdm	$⊢ (M : X \times X ⟶ [0, x] \land y \in X \land z \in X) \to y M z \in [0, x]$
102	101	3expa	$⊢ ((M : X \times X ⟶ [0, x] \land y \in X) \land z \in X) \to y M z \in [0, x]$
103	102	adantlll	$⊢ ((((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \land z \in X) \to y M z \in [0, x]$
104		elicc2	$⊢ (0 \in ℝ \land x \in ℝ) \to (y M z \in [0, x] \leftrightarrow (y M z \in ℝ \land 0 \leq y M z \land y M z \leq x))$
105	2 88 104	sylancr	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to (y M z \in [0, x] \leftrightarrow (y M z \in ℝ \land 0 \leq y M z \land y M z \leq x))$
106	105	adantr	$⊢ ((((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \land z \in X) \to (y M z \in [0, x] \leftrightarrow (y M z \in ℝ \land 0 \leq y M z \land y M z \leq x))$
107	103 106	mpbid	$⊢ ((((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \land z \in X) \to (y M z \in ℝ \land 0 \leq y M z \land y M z \leq x)$
108	107	simp1d	$⊢ ((((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \land z \in X) \to y M z \in ℝ$
109	88	adantr	$⊢ ((((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \land z \in X) \to x \in ℝ$
110		peano2re	$⊢ x \in ℝ \to x + 1 \in ℝ$
111	88 110	syl	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to x + 1 \in ℝ$
112	111	adantr	$⊢ ((((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \land z \in X) \to x + 1 \in ℝ$
113	107	simp3d	$⊢ ((((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \land z \in X) \to y M z \leq x$
114	109	ltp1d	$⊢ ((((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \land z \in X) \to x < x + 1$
115	108 109 112 113 114	lelttrd	$⊢ ((((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \land z \in X) \to y M z < x + 1$
116	115	ralrimiva	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to \forall z \in X y M z < x + 1$
117		rabid2	$⊢ X = \{z \in X \| y M z < x + 1\} \leftrightarrow \forall z \in X y M z < x + 1$
118	116 117	sylibr	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to X = \{z \in X \| y M z < x + 1\}$
119	89 52	syl	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to M \in ∞Met (X)$
120	111	rexrd	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to x + 1 \in ℝ^{*}$
121		blval	$⊢ (M \in ∞Met (X) \land y \in X \land x + 1 \in ℝ^{*}) \to y ball (M) (x + 1) = \{z \in X \| y M z < x + 1\}$
122	119 90 120 121	syl3anc	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to y ball (M) (x + 1) = \{z \in X \| y M z < x + 1\}$
123	118 122	eqtr4d	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to X = y ball (M) (x + 1)$
124		oveq2	$⊢ r = x + 1 \to y ball (M) r = y ball (M) (x + 1)$
125	124	rspceeqv	$⊢ (x + 1 \in ℝ^{+} \land X = y ball (M) (x + 1)) \to \exists r \in ℝ^{+} X = y ball (M) r$
126	100 123 125	syl2anc	$⊢ (((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \land y \in X) \to \exists r \in ℝ^{+} X = y ball (M) r$
127	126	ralrimiva	$⊢ ((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \to \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r$
128		isbnd	$⊢ M \in Bnd (X) \leftrightarrow (M \in Met (X) \land \forall y \in X \exists r \in ℝ^{+} X = y ball (M) r)$
129	87 127 128	sylanbrc	$⊢ ((M \in Met (X) \land x \in ℝ) \land M : X \times X ⟶ [0, x]) \to M \in Bnd (X)$
130	129	r19.29an	$⊢ (M \in Met (X) \land \exists x \in ℝ M : X \times X ⟶ [0, x]) \to M \in Bnd (X)$
131	86 130	impbii	$⊢ M \in Bnd (X) \leftrightarrow (M \in Met (X) \land \exists x \in ℝ M : X \times X ⟶ [0, x])$

Metamath Proof Explorer

Theorem isbnd3

Proof