Metamath Proof Explorer


Theorem isbnd3b

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

Ref Expression
Assertion isbnd3b
|- ( M e. ( Bnd ` X ) <-> ( M e. ( Met ` X ) /\ E. x e. RR A. y e. X A. z e. X ( y M z ) <_ x ) )

Proof

Step Hyp Ref Expression
1 isbnd3
 |-  ( M e. ( Bnd ` X ) <-> ( M e. ( Met ` X ) /\ E. x e. RR M : ( X X. X ) --> ( 0 [,] x ) ) )
2 metf
 |-  ( M e. ( Met ` X ) -> M : ( X X. X ) --> RR )
3 2 adantr
 |-  ( ( M e. ( Met ` X ) /\ x e. RR ) -> M : ( X X. X ) --> RR )
4 ffn
 |-  ( M : ( X X. X ) --> RR -> M Fn ( X X. X ) )
5 ffnov
 |-  ( M : ( X X. X ) --> ( 0 [,] x ) <-> ( M Fn ( X X. X ) /\ A. y e. X A. z e. X ( y M z ) e. ( 0 [,] x ) ) )
6 5 baib
 |-  ( M Fn ( X X. X ) -> ( M : ( X X. X ) --> ( 0 [,] x ) <-> A. y e. X A. z e. X ( y M z ) e. ( 0 [,] x ) ) )
7 3 4 6 3syl
 |-  ( ( M e. ( Met ` X ) /\ x e. RR ) -> ( M : ( X X. X ) --> ( 0 [,] x ) <-> A. y e. X A. z e. X ( y M z ) e. ( 0 [,] x ) ) )
8 0red
 |-  ( ( ( M e. ( Met ` X ) /\ x e. RR ) /\ ( y e. X /\ z e. X ) ) -> 0 e. RR )
9 simplr
 |-  ( ( ( M e. ( Met ` X ) /\ x e. RR ) /\ ( y e. X /\ z e. X ) ) -> x e. RR )
10 metcl
 |-  ( ( M e. ( Met ` X ) /\ y e. X /\ z e. X ) -> ( y M z ) e. RR )
11 10 3expb
 |-  ( ( M e. ( Met ` X ) /\ ( y e. X /\ z e. X ) ) -> ( y M z ) e. RR )
12 11 adantlr
 |-  ( ( ( M e. ( Met ` X ) /\ x e. RR ) /\ ( y e. X /\ z e. X ) ) -> ( y M z ) e. RR )
13 metge0
 |-  ( ( M e. ( Met ` X ) /\ y e. X /\ z e. X ) -> 0 <_ ( y M z ) )
14 13 3expb
 |-  ( ( M e. ( Met ` X ) /\ ( y e. X /\ z e. X ) ) -> 0 <_ ( y M z ) )
15 14 adantlr
 |-  ( ( ( M e. ( Met ` X ) /\ x e. RR ) /\ ( y e. X /\ z e. X ) ) -> 0 <_ ( y M z ) )
16 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 ) ) )
17 df-3an
 |-  ( ( ( y M z ) e. RR /\ 0 <_ ( y M z ) /\ ( y M z ) <_ x ) <-> ( ( ( y M z ) e. RR /\ 0 <_ ( y M z ) ) /\ ( y M z ) <_ x ) )
18 16 17 bitrdi
 |-  ( ( 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 ) ) )
19 18 baibd
 |-  ( ( ( 0 e. RR /\ x e. RR ) /\ ( ( y M z ) e. RR /\ 0 <_ ( y M z ) ) ) -> ( ( y M z ) e. ( 0 [,] x ) <-> ( y M z ) <_ x ) )
20 8 9 12 15 19 syl22anc
 |-  ( ( ( M e. ( Met ` X ) /\ x e. RR ) /\ ( y e. X /\ z e. X ) ) -> ( ( y M z ) e. ( 0 [,] x ) <-> ( y M z ) <_ x ) )
21 20 2ralbidva
 |-  ( ( M e. ( Met ` X ) /\ x e. RR ) -> ( A. y e. X A. z e. X ( y M z ) e. ( 0 [,] x ) <-> A. y e. X A. z e. X ( y M z ) <_ x ) )
22 7 21 bitrd
 |-  ( ( M e. ( Met ` X ) /\ x e. RR ) -> ( M : ( X X. X ) --> ( 0 [,] x ) <-> A. y e. X A. z e. X ( y M z ) <_ x ) )
23 22 rexbidva
 |-  ( M e. ( Met ` X ) -> ( E. x e. RR M : ( X X. X ) --> ( 0 [,] x ) <-> E. x e. RR A. y e. X A. z e. X ( y M z ) <_ x ) )
24 23 pm5.32i
 |-  ( ( M e. ( Met ` X ) /\ E. x e. RR M : ( X X. X ) --> ( 0 [,] x ) ) <-> ( M e. ( Met ` X ) /\ E. x e. RR A. y e. X A. z e. X ( y M z ) <_ x ) )
25 1 24 bitri
 |-  ( M e. ( Bnd ` X ) <-> ( M e. ( Met ` X ) /\ E. x e. RR A. y e. X A. z e. X ( y M z ) <_ x ) )