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