Metamath Proof Explorer

Theorem metequiv2

Description: If there is a sequence of radii approaching zero for which the balls of both metrics coincide, then the generated topologies are equivalent. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses metequiv.3 
|- J = ( MetOpen ` C )
metequiv.4 
|- K = ( MetOpen ` D )
Assertion metequiv2 
|- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( A. x e. X A. r e. RR+ E. s e. RR+ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) -> J = K ) )

Proof

Step Hyp Ref Expression
1 metequiv.3 
 |-  J = ( MetOpen ` C )
2 metequiv.4 
 |-  K = ( MetOpen ` D )
3 simprrr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) )
4 simplll 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> C e. ( *Met ` X ) )
5 simplr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> x e. X )
6 simprlr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> s e. RR+ )
7 6 rpxrd 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> s e. RR* )
8 simprll 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> r e. RR+ )
9 8 rpxrd 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> r e. RR* )
10 simprrl 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> s <_ r )
11 ssbl 
 |-  ( ( ( C e. ( *Met ` X ) /\ x e. X ) /\ ( s e. RR* /\ r e. RR* ) /\ s <_ r ) -> ( x ( ball ` C ) s ) C_ ( x ( ball ` C ) r ) )
12 4 5 7 9 10 11 syl221anc 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> ( x ( ball ` C ) s ) C_ ( x ( ball ` C ) r ) )
13 3 12 eqsstrrd 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) )
14 simpllr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> D e. ( *Met ` X ) )
15 ssbl 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( s e. RR* /\ r e. RR* ) /\ s <_ r ) -> ( x ( ball ` D ) s ) C_ ( x ( ball ` D ) r ) )
16 14 5 7 9 10 15 syl221anc 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> ( x ( ball ` D ) s ) C_ ( x ( ball ` D ) r ) )
17 3 16 eqsstrd 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) )
18 13 17 jca 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( ( r e. RR+ /\ s e. RR+ ) /\ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) ) ) -> ( ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) ) )
19 18 expr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( r e. RR+ /\ s e. RR+ ) ) -> ( ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) -> ( ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) ) ) )
20 19 anassrs 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ r e. RR+ ) /\ s e. RR+ ) -> ( ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) -> ( ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) ) ) )
21 20 reximdva 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ r e. RR+ ) -> ( E. s e. RR+ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) -> E. s e. RR+ ( ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) ) ) )
22 r19.40 
 |-  ( E. s e. RR+ ( ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) ) -> ( E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ E. s e. RR+ ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) ) )
23 21 22 syl6 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ r e. RR+ ) -> ( E. s e. RR+ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) -> ( E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ E. s e. RR+ ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) ) ) )
24 23 ralimdva 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) -> ( A. r e. RR+ E. s e. RR+ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) -> A. r e. RR+ ( E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ E. s e. RR+ ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) ) ) )
25 r19.26 
 |-  ( A. r e. RR+ ( E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ E. s e. RR+ ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) ) <-> ( A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ A. r e. RR+ E. s e. RR+ ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) ) )
26 24 25 imbitrdi 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) -> ( A. r e. RR+ E. s e. RR+ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) -> ( A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ A. r e. RR+ E. s e. RR+ ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) ) ) )
27 26 ralimdva 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( A. x e. X A. r e. RR+ E. s e. RR+ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) -> A. x e. X ( A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ A. r e. RR+ E. s e. RR+ ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) ) ) )
28 1 2 metequiv 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( J = K <-> A. x e. X ( A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ A. r e. RR+ E. s e. RR+ ( x ( ball ` C ) s ) C_ ( x ( ball ` D ) r ) ) ) )
29 27 28 sylibrd 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( A. x e. X A. r e. RR+ E. s e. RR+ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) -> J = K ) )