Metamath Proof Explorer


Theorem 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 Bnd X M Met X x M : X × X 0 x

Proof

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