Metamath Proof Explorer


Theorem 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 TotBnd X M Bnd X

Proof

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