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 e. ( Bnd ` X ) <-> ( M e. ( Met ` X ) /\ E. x e. RR M : ( X X. X ) --> ( 0 [,] x ) ) )

Proof

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