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