totbndbnd

Description: A totally bounded metric space is bounded. This theorem fails for extended metrics - a bounded extended metric is a metric, but there are totally bounded extended metrics that are not metrics (if we were to weaken istotbnd to only require that M be an extended metric). A counterexample is the discrete extended metric (assigning distinct points distance +oo ) on a finite set. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

		Ref	Expression
	Assertion	totbndbnd	$⊢ M \in TotBnd (X) \to M \in Bnd (X)$

Proof

Step	Hyp	Ref	Expression
1		totbndmet	$⊢ M \in TotBnd (X) \to M \in Met (X)$
2		1rp	$⊢ 1 \in ℝ^{+}$
3		istotbnd3	$⊢ M \in TotBnd (X) \leftrightarrow (M \in Met (X) \land \forall d \in ℝ^{+} \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) d) = X)$
4	3	simprbi	$⊢ M \in TotBnd (X) \to \forall d \in ℝ^{+} \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) d) = X$
5		oveq2	$⊢ d = 1 \to x ball (M) d = x ball (M) 1$
6	5	iuneq2d	$⊢ d = 1 \to ⋃_{x \in v} (x ball (M) d) = ⋃_{x \in v} (x ball (M) 1)$
7	6	eqeq1d	$⊢ d = 1 \to (⋃_{x \in v} (x ball (M) d) = X \leftrightarrow ⋃_{x \in v} (x ball (M) 1) = X)$
8	7	rexbidv	$⊢ d = 1 \to (\exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) d) = X \leftrightarrow \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) 1) = X)$
9	8	rspcv	$⊢ 1 \in ℝ^{+} \to (\forall d \in ℝ^{+} \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) d) = X \to \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) 1) = X)$
10	2 4 9	mpsyl	$⊢ M \in TotBnd (X) \to \exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) 1) = X$
11		simplll	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to M \in Met (X)$
12		elfpw	$⊢ v \in (𝒫 X \cap Fin) \leftrightarrow (v \subseteq X \land v \in Fin)$
13	12	simplbi	$⊢ v \in (𝒫 X \cap Fin) \to v \subseteq X$
14	13	ad2antrl	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to v \subseteq X$
15	14	sselda	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to z \in X$
16		simpllr	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to y \in X$
17		metcl	$⊢ (M \in Met (X) \land z \in X \land y \in X) \to z M y \in ℝ$
18	11 15 16 17	syl3anc	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to z M y \in ℝ$
19		metge0	$⊢ (M \in Met (X) \land z \in X \land y \in X) \to 0 \leq z M y$
20	11 15 16 19	syl3anc	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to 0 \leq z M y$
21	18 20	ge0p1rpd	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to (z M y) + 1 \in ℝ^{+}$
22	21	fmpttd	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to (z \in v ⟼ (z M y) + 1) : v ⟶ ℝ^{+}$
23	22	frnd	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to ran (z \in v ⟼ (z M y) + 1) \subseteq ℝ^{+}$
24	12	simprbi	$⊢ v \in (𝒫 X \cap Fin) \to v \in Fin$
25		mptfi	$⊢ v \in Fin \to (z \in v ⟼ (z M y) + 1) \in Fin$
26		rnfi	$⊢ (z \in v ⟼ (z M y) + 1) \in Fin \to ran (z \in v ⟼ (z M y) + 1) \in Fin$
27	24 25 26	3syl	$⊢ v \in (𝒫 X \cap Fin) \to ran (z \in v ⟼ (z M y) + 1) \in Fin$
28	27	ad2antrl	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to ran (z \in v ⟼ (z M y) + 1) \in Fin$
29		simplr	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to y \in X$
30		simprr	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to ⋃_{x \in v} (x ball (M) 1) = X$
31	29 30	eleqtrrd	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to y \in ⋃_{x \in v} (x ball (M) 1)$
32		ne0i	$⊢ y \in ⋃_{x \in v} (x ball (M) 1) \to ⋃_{x \in v} (x ball (M) 1) \neq \emptyset$
33		dm0rn0	$⊢ dom (z \in v ⟼ (z M y) + 1) = \emptyset \leftrightarrow ran (z \in v ⟼ (z M y) + 1) = \emptyset$
34		ovex	$⊢ (z M y) + 1 \in V$
35		eqid	$⊢ (z \in v ⟼ (z M y) + 1) = (z \in v ⟼ (z M y) + 1)$
36	34 35	dmmpti	$⊢ dom (z \in v ⟼ (z M y) + 1) = v$
37	36	eqeq1i	$⊢ dom (z \in v ⟼ (z M y) + 1) = \emptyset \leftrightarrow v = \emptyset$
38		iuneq1	$⊢ v = \emptyset \to ⋃_{x \in v} (x ball (M) 1) = ⋃_{x \in \emptyset} (x ball (M) 1)$
39	37 38	sylbi	$⊢ dom (z \in v ⟼ (z M y) + 1) = \emptyset \to ⋃_{x \in v} (x ball (M) 1) = ⋃_{x \in \emptyset} (x ball (M) 1)$
40		0iun	$⊢ ⋃_{x \in \emptyset} (x ball (M) 1) = \emptyset$
41	39 40	eqtrdi	$⊢ dom (z \in v ⟼ (z M y) + 1) = \emptyset \to ⋃_{x \in v} (x ball (M) 1) = \emptyset$
42	33 41	sylbir	$⊢ ran (z \in v ⟼ (z M y) + 1) = \emptyset \to ⋃_{x \in v} (x ball (M) 1) = \emptyset$
43	42	necon3i	$⊢ ⋃_{x \in v} (x ball (M) 1) \neq \emptyset \to ran (z \in v ⟼ (z M y) + 1) \neq \emptyset$
44	31 32 43	3syl	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to ran (z \in v ⟼ (z M y) + 1) \neq \emptyset$
45		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
46	23 45	sstrdi	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to ran (z \in v ⟼ (z M y) + 1) \subseteq ℝ$
47		ltso	$⊢ < Or ℝ$
48		fisupcl	$⊢ (< Or ℝ \land (ran (z \in v ⟼ (z M y) + 1) \in Fin \land ran (z \in v ⟼ (z M y) + 1) \neq \emptyset \land ran (z \in v ⟼ (z M y) + 1) \subseteq ℝ)) \to sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \in ran (z \in v ⟼ (z M y) + 1)$
49	47 48	mpan	$⊢ (ran (z \in v ⟼ (z M y) + 1) \in Fin \land ran (z \in v ⟼ (z M y) + 1) \neq \emptyset \land ran (z \in v ⟼ (z M y) + 1) \subseteq ℝ) \to sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \in ran (z \in v ⟼ (z M y) + 1)$
50	28 44 46 49	syl3anc	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \in ran (z \in v ⟼ (z M y) + 1)$
51	23 50	sseldd	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \in ℝ^{+}$
52		metxmet	$⊢ M \in Met (X) \to M \in ∞Met (X)$
53	52	ad2antrr	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to M \in ∞Met (X)$
54	53	adantr	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to M \in ∞Met (X)$
55		1red	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to 1 \in ℝ$
56	46 50	sseldd	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \in ℝ$
57	56	adantr	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \in ℝ$
58	46	adantr	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to ran (z \in v ⟼ (z M y) + 1) \subseteq ℝ$
59	44	adantr	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to ran (z \in v ⟼ (z M y) + 1) \neq \emptyset$
60	28	adantr	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to ran (z \in v ⟼ (z M y) + 1) \in Fin$
61		fimaxre2	$⊢ (ran (z \in v ⟼ (z M y) + 1) \subseteq ℝ \land ran (z \in v ⟼ (z M y) + 1) \in Fin) \to \exists d \in ℝ \forall w \in ran (z \in v ⟼ (z M y) + 1) w \leq d$
62	58 60 61	syl2anc	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to \exists d \in ℝ \forall w \in ran (z \in v ⟼ (z M y) + 1) w \leq d$
63	35	elrnmpt1	$⊢ (z \in v \land (z M y) + 1 \in V) \to (z M y) + 1 \in ran (z \in v ⟼ (z M y) + 1)$
64	34 63	mpan2	$⊢ z \in v \to (z M y) + 1 \in ran (z \in v ⟼ (z M y) + 1)$
65	64	adantl	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to (z M y) + 1 \in ran (z \in v ⟼ (z M y) + 1)$
66		suprub	$⊢ ((ran (z \in v ⟼ (z M y) + 1) \subseteq ℝ \land ran (z \in v ⟼ (z M y) + 1) \neq \emptyset \land \exists d \in ℝ \forall w \in ran (z \in v ⟼ (z M y) + 1) w \leq d) \land (z M y) + 1 \in ran (z \in v ⟼ (z M y) + 1)) \to (z M y) + 1 \leq sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
67	58 59 62 65 66	syl31anc	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to (z M y) + 1 \leq sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
68		leaddsub	$⊢ (z M y \in ℝ \land 1 \in ℝ \land sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \in ℝ) \to ((z M y) + 1 \leq sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \leftrightarrow z M y \leq sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) - 1)$
69	18 55 57 68	syl3anc	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to ((z M y) + 1 \leq sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \leftrightarrow z M y \leq sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) - 1)$
70	67 69	mpbid	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to z M y \leq sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) - 1$
71		blss2	$⊢ ((M \in ∞Met (X) \land z \in X \land y \in X) \land (1 \in ℝ \land sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \in ℝ \land z M y \leq sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) - 1)) \to z ball (M) 1 \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
72	54 15 16 55 57 70 71	syl33anc	$⊢ (((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \land z \in v) \to z ball (M) 1 \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
73	72	ralrimiva	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to \forall z \in v z ball (M) 1 \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
74		nfcv	$⊢ \underline{Ⅎ} z (x ball (M) 1)$
75		nfcv	$⊢ \underline{Ⅎ} z y$
76		nfcv	$⊢ \underline{Ⅎ} z ball (M)$
77		nfmpt1	$⊢ \underline{Ⅎ} z (z \in v ⟼ (z M y) + 1)$
78	77	nfrn	$⊢ \underline{Ⅎ} z ran (z \in v ⟼ (z M y) + 1)$
79		nfcv	$⊢ \underline{Ⅎ} z ℝ$
80		nfcv	$⊢ \underline{Ⅎ} z <$
81	78 79 80	nfsup	$⊢ \underline{Ⅎ} z sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
82	75 76 81	nfov	$⊢ \underline{Ⅎ} z (y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <))$
83	74 82	nfss	$⊢ Ⅎ z x ball (M) 1 \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
84		nfv	$⊢ Ⅎ x z ball (M) 1 \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
85		oveq1	$⊢ x = z \to x ball (M) 1 = z ball (M) 1$
86	85	sseq1d	$⊢ x = z \to (x ball (M) 1 \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \leftrightarrow z ball (M) 1 \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <))$
87	83 84 86	cbvralw	$⊢ \forall x \in v x ball (M) 1 \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \leftrightarrow \forall z \in v z ball (M) 1 \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
88	73 87	sylibr	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to \forall x \in v x ball (M) 1 \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
89		iunss	$⊢ ⋃_{x \in v} (x ball (M) 1) \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \leftrightarrow \forall x \in v x ball (M) 1 \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
90	88 89	sylibr	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to ⋃_{x \in v} (x ball (M) 1) \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
91	30 90	eqsstrrd	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to X \subseteq y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
92	51	rpxrd	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \in ℝ^{*}$
93		blssm	$⊢ (M \in ∞Met (X) \land y \in X \land sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \in ℝ^{*}) \to y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \subseteq X$
94	53 29 92 93	syl3anc	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \subseteq X$
95	91 94	eqssd	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to X = y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
96		oveq2	$⊢ d = sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \to y ball (M) d = y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)$
97	96	rspceeqv	$⊢ (sup (ran (z \in v ⟼ (z M y) + 1) ℝ <) \in ℝ^{+} \land X = y ball (M) sup (ran (z \in v ⟼ (z M y) + 1) ℝ <)) \to \exists d \in ℝ^{+} X = y ball (M) d$
98	51 95 97	syl2anc	$⊢ ((M \in Met (X) \land y \in X) \land (v \in (𝒫 X \cap Fin) \land ⋃_{x \in v} (x ball (M) 1) = X)) \to \exists d \in ℝ^{+} X = y ball (M) d$
99	98	rexlimdvaa	$⊢ (M \in Met (X) \land y \in X) \to (\exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) 1) = X \to \exists d \in ℝ^{+} X = y ball (M) d)$
100	99	ralrimdva	$⊢ M \in Met (X) \to (\exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) 1) = X \to \forall y \in X \exists d \in ℝ^{+} X = y ball (M) d)$
101		isbnd	$⊢ M \in Bnd (X) \leftrightarrow (M \in Met (X) \land \forall y \in X \exists d \in ℝ^{+} X = y ball (M) d)$
102	101	baib	$⊢ M \in Met (X) \to (M \in Bnd (X) \leftrightarrow \forall y \in X \exists d \in ℝ^{+} X = y ball (M) d)$
103	100 102	sylibrd	$⊢ M \in Met (X) \to (\exists v \in (𝒫 X \cap Fin) ⋃_{x \in v} (x ball (M) 1) = X \to M \in Bnd (X))$
104	1 10 103	sylc	$⊢ M \in TotBnd (X) \to M \in Bnd (X)$

Metamath Proof Explorer

Theorem totbndbnd

Proof