This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )