Metamath Proof Explorer

Theorem isbndx

Description: A "bounded extended metric" (meaning that it satisfies the same condition as a bounded metric, but with "metric" replaced with "extended metric") is a metric and thus is bounded in the conventional sense. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion isbndx 
|- ( M e. ( Bnd ` X ) <-> ( M e. ( *Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) )

Proof

Step Hyp Ref Expression
1 isbnd 
 |-  ( M e. ( Bnd ` X ) <-> ( M e. ( Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) )
2 metxmet 
 |-  ( M e. ( Met ` X ) -> M e. ( *Met ` X ) )
3 simpr 
 |-  ( ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) /\ M e. ( *Met ` X ) ) -> M e. ( *Met ` X ) )
4 xmetf 
 |-  ( M e. ( *Met ` X ) -> M : ( X X. X ) --> RR* )
5 ffn 
 |-  ( M : ( X X. X ) --> RR* -> M Fn ( X X. X ) )
6 3 4 5 3syl 
 |-  ( ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) /\ M e. ( *Met ` X ) ) -> M Fn ( X X. X ) )
7 simprr 
 |-  ( ( ( M e. ( *Met ` X ) /\ x e. X ) /\ ( r e. RR+ /\ X = ( x ( ball ` M ) r ) ) ) -> X = ( x ( ball ` M ) r ) )
8 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
9 eqid 
 |-  ( `' M " RR ) = ( `' M " RR )
10 9 blssec 
 |-  ( ( M e. ( *Met ` X ) /\ x e. X /\ r e. RR* ) -> ( x ( ball ` M ) r ) C_ [ x ] ( `' M " RR ) )
11 10 3expa 
 |-  ( ( ( M e. ( *Met ` X ) /\ x e. X ) /\ r e. RR* ) -> ( x ( ball ` M ) r ) C_ [ x ] ( `' M " RR ) )
12 8 11 sylan2 
 |-  ( ( ( M e. ( *Met ` X ) /\ x e. X ) /\ r e. RR+ ) -> ( x ( ball ` M ) r ) C_ [ x ] ( `' M " RR ) )
13 12 adantrr 
 |-  ( ( ( M e. ( *Met ` X ) /\ x e. X ) /\ ( r e. RR+ /\ X = ( x ( ball ` M ) r ) ) ) -> ( x ( ball ` M ) r ) C_ [ x ] ( `' M " RR ) )
14 7 13 eqsstrd 
 |-  ( ( ( M e. ( *Met ` X ) /\ x e. X ) /\ ( r e. RR+ /\ X = ( x ( ball ` M ) r ) ) ) -> X C_ [ x ] ( `' M " RR ) )
15 14 sselda 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ x e. X ) /\ ( r e. RR+ /\ X = ( x ( ball ` M ) r ) ) ) /\ y e. X ) -> y e. [ x ] ( `' M " RR ) )
16 vex 
 |-  y e. _V
17 vex 
 |-  x e. _V
18 16 17 elec 
 |-  ( y e. [ x ] ( `' M " RR ) <-> x ( `' M " RR ) y )
19 15 18 sylib 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ x e. X ) /\ ( r e. RR+ /\ X = ( x ( ball ` M ) r ) ) ) /\ y e. X ) -> x ( `' M " RR ) y )
20 9 xmeterval 
 |-  ( M e. ( *Met ` X ) -> ( x ( `' M " RR ) y <-> ( x e. X /\ y e. X /\ ( x M y ) e. RR ) ) )
21 20 ad3antrrr 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ x e. X ) /\ ( r e. RR+ /\ X = ( x ( ball ` M ) r ) ) ) /\ y e. X ) -> ( x ( `' M " RR ) y <-> ( x e. X /\ y e. X /\ ( x M y ) e. RR ) ) )
22 19 21 mpbid 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ x e. X ) /\ ( r e. RR+ /\ X = ( x ( ball ` M ) r ) ) ) /\ y e. X ) -> ( x e. X /\ y e. X /\ ( x M y ) e. RR ) )
23 22 simp3d 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ x e. X ) /\ ( r e. RR+ /\ X = ( x ( ball ` M ) r ) ) ) /\ y e. X ) -> ( x M y ) e. RR )
24 23 ralrimiva 
 |-  ( ( ( M e. ( *Met ` X ) /\ x e. X ) /\ ( r e. RR+ /\ X = ( x ( ball ` M ) r ) ) ) -> A. y e. X ( x M y ) e. RR )
25 24 rexlimdvaa 
 |-  ( ( M e. ( *Met ` X ) /\ x e. X ) -> ( E. r e. RR+ X = ( x ( ball ` M ) r ) -> A. y e. X ( x M y ) e. RR ) )
26 25 ralimdva 
 |-  ( M e. ( *Met ` X ) -> ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) -> A. x e. X A. y e. X ( x M y ) e. RR ) )
27 26 impcom 
 |-  ( ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) /\ M e. ( *Met ` X ) ) -> A. x e. X A. y e. X ( x M y ) e. RR )
28 ffnov 
 |-  ( M : ( X X. X ) --> RR <-> ( M Fn ( X X. X ) /\ A. x e. X A. y e. X ( x M y ) e. RR ) )
29 6 27 28 sylanbrc 
 |-  ( ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) /\ M e. ( *Met ` X ) ) -> M : ( X X. X ) --> RR )
30 ismet2 
 |-  ( M e. ( Met ` X ) <-> ( M e. ( *Met ` X ) /\ M : ( X X. X ) --> RR ) )
31 3 29 30 sylanbrc 
 |-  ( ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) /\ M e. ( *Met ` X ) ) -> M e. ( Met ` X ) )
32 31 ex 
 |-  ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) -> ( M e. ( *Met ` X ) -> M e. ( Met ` X ) ) )
33 2 32 impbid2 
 |-  ( A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) -> ( M e. ( Met ` X ) <-> M e. ( *Met ` X ) ) )
34 33 pm5.32ri 
 |-  ( ( M e. ( Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) <-> ( M e. ( *Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) )
35 1 34 bitri 
 |-  ( M e. ( Bnd ` X ) <-> ( M e. ( *Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) )