Metamath Proof Explorer

Theorem stdbdmopn

Description: The standard bounded metric corresponding to C generates the same topology as C . (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses stdbdmet.1 
|- D = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) )
stdbdmopn.2 
|- J = ( MetOpen ` C )
Assertion stdbdmopn 
|- ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> J = ( MetOpen ` D ) )

Proof

Step Hyp Ref Expression
1 stdbdmet.1 
 |-  D = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) )
2 stdbdmopn.2 
 |-  J = ( MetOpen ` C )
3 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
4 3 ad2antll 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> r e. RR* )
5 simpl2 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> R e. RR* )
6 4 5 ifcld 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> if ( r <_ R , r , R ) e. RR* )
7 rpre 
 |-  ( r e. RR+ -> r e. RR )
8 7 ad2antll 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> r e. RR )
9 rpgt0 
 |-  ( r e. RR+ -> 0 < r )
10 9 ad2antll 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> 0 < r )
11 simpl3 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> 0 < R )
12 breq2 
 |-  ( r = if ( r <_ R , r , R ) -> ( 0 < r <-> 0 < if ( r <_ R , r , R ) ) )
13 breq2 
 |-  ( R = if ( r <_ R , r , R ) -> ( 0 < R <-> 0 < if ( r <_ R , r , R ) ) )
14 12 13 ifboth 
 |-  ( ( 0 < r /\ 0 < R ) -> 0 < if ( r <_ R , r , R ) )
15 10 11 14 syl2anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> 0 < if ( r <_ R , r , R ) )
16 0xr 
 |-  0 e. RR*
17 xrltle 
 |-  ( ( 0 e. RR* /\ if ( r <_ R , r , R ) e. RR* ) -> ( 0 < if ( r <_ R , r , R ) -> 0 <_ if ( r <_ R , r , R ) ) )
18 16 6 17 sylancr 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> ( 0 < if ( r <_ R , r , R ) -> 0 <_ if ( r <_ R , r , R ) ) )
19 15 18 mpd 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> 0 <_ if ( r <_ R , r , R ) )
20 xrmin1 
 |-  ( ( r e. RR* /\ R e. RR* ) -> if ( r <_ R , r , R ) <_ r )
21 4 5 20 syl2anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> if ( r <_ R , r , R ) <_ r )
22 xrrege0 
 |-  ( ( ( if ( r <_ R , r , R ) e. RR* /\ r e. RR ) /\ ( 0 <_ if ( r <_ R , r , R ) /\ if ( r <_ R , r , R ) <_ r ) ) -> if ( r <_ R , r , R ) e. RR )
23 6 8 19 21 22 syl22anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> if ( r <_ R , r , R ) e. RR )
24 23 15 elrpd 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> if ( r <_ R , r , R ) e. RR+ )
25 simprl 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> z e. X )
26 xrmin2 
 |-  ( ( r e. RR* /\ R e. RR* ) -> if ( r <_ R , r , R ) <_ R )
27 4 5 26 syl2anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> if ( r <_ R , r , R ) <_ R )
28 25 6 27 3jca 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> ( z e. X /\ if ( r <_ R , r , R ) e. RR* /\ if ( r <_ R , r , R ) <_ R ) )
29 1 stdbdbl 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ if ( r <_ R , r , R ) e. RR* /\ if ( r <_ R , r , R ) <_ R ) ) -> ( z ( ball ` D ) if ( r <_ R , r , R ) ) = ( z ( ball ` C ) if ( r <_ R , r , R ) ) )
30 28 29 syldan 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> ( z ( ball ` D ) if ( r <_ R , r , R ) ) = ( z ( ball ` C ) if ( r <_ R , r , R ) ) )
31 30 eqcomd 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> ( z ( ball ` C ) if ( r <_ R , r , R ) ) = ( z ( ball ` D ) if ( r <_ R , r , R ) ) )
32 breq1 
 |-  ( s = if ( r <_ R , r , R ) -> ( s <_ r <-> if ( r <_ R , r , R ) <_ r ) )
33 oveq2 
 |-  ( s = if ( r <_ R , r , R ) -> ( z ( ball ` C ) s ) = ( z ( ball ` C ) if ( r <_ R , r , R ) ) )
34 oveq2 
 |-  ( s = if ( r <_ R , r , R ) -> ( z ( ball ` D ) s ) = ( z ( ball ` D ) if ( r <_ R , r , R ) ) )
35 33 34 eqeq12d 
 |-  ( s = if ( r <_ R , r , R ) -> ( ( z ( ball ` C ) s ) = ( z ( ball ` D ) s ) <-> ( z ( ball ` C ) if ( r <_ R , r , R ) ) = ( z ( ball ` D ) if ( r <_ R , r , R ) ) ) )
36 32 35 anbi12d 
 |-  ( s = if ( r <_ R , r , R ) -> ( ( s <_ r /\ ( z ( ball ` C ) s ) = ( z ( ball ` D ) s ) ) <-> ( if ( r <_ R , r , R ) <_ r /\ ( z ( ball ` C ) if ( r <_ R , r , R ) ) = ( z ( ball ` D ) if ( r <_ R , r , R ) ) ) ) )
37 36 rspcev 
 |-  ( ( if ( r <_ R , r , R ) e. RR+ /\ ( if ( r <_ R , r , R ) <_ r /\ ( z ( ball ` C ) if ( r <_ R , r , R ) ) = ( z ( ball ` D ) if ( r <_ R , r , R ) ) ) ) -> E. s e. RR+ ( s <_ r /\ ( z ( ball ` C ) s ) = ( z ( ball ` D ) s ) ) )
38 24 21 31 37 syl12anc 
 |-  ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( z e. X /\ r e. RR+ ) ) -> E. s e. RR+ ( s <_ r /\ ( z ( ball ` C ) s ) = ( z ( ball ` D ) s ) ) )
39 38 ralrimivva 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> A. z e. X A. r e. RR+ E. s e. RR+ ( s <_ r /\ ( z ( ball ` C ) s ) = ( z ( ball ` D ) s ) ) )
40 simp1 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> C e. ( *Met ` X ) )
41 1 stdbdxmet 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> D e. ( *Met ` X ) )
42 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
43 2 42 metequiv2 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( A. z e. X A. r e. RR+ E. s e. RR+ ( s <_ r /\ ( z ( ball ` C ) s ) = ( z ( ball ` D ) s ) ) -> J = ( MetOpen ` D ) ) )
44 40 41 43 syl2anc 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> ( A. z e. X A. r e. RR+ E. s e. RR+ ( s <_ r /\ ( z ( ball ` C ) s ) = ( z ( ball ` D ) s ) ) -> J = ( MetOpen ` D ) ) )
45 39 44 mpd 
 |-  ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> J = ( MetOpen ` D ) )