Step |
Hyp |
Ref |
Expression |
1 |
|
metequiv.3 |
|- J = ( MetOpen ` C ) |
2 |
|
metequiv.4 |
|- K = ( MetOpen ` D ) |
3 |
|
metss2.1 |
|- ( ph -> C e. ( Met ` X ) ) |
4 |
|
metss2.2 |
|- ( ph -> D e. ( Met ` X ) ) |
5 |
|
metss2.3 |
|- ( ph -> R e. RR+ ) |
6 |
|
metss2.4 |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) ) |
7 |
4
|
ad2antrr |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> D e. ( Met ` X ) ) |
8 |
|
simplrl |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> x e. X ) |
9 |
|
simpr |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> y e. X ) |
10 |
|
metcl |
|- ( ( D e. ( Met ` X ) /\ x e. X /\ y e. X ) -> ( x D y ) e. RR ) |
11 |
7 8 9 10
|
syl3anc |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( x D y ) e. RR ) |
12 |
|
simplrr |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> S e. RR+ ) |
13 |
12
|
rpred |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> S e. RR ) |
14 |
5
|
ad2antrr |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> R e. RR+ ) |
15 |
11 13 14
|
ltmuldiv2d |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( ( R x. ( x D y ) ) < S <-> ( x D y ) < ( S / R ) ) ) |
16 |
6
|
anassrs |
|- ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( x C y ) <_ ( R x. ( x D y ) ) ) |
17 |
16
|
adantlrr |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( x C y ) <_ ( R x. ( x D y ) ) ) |
18 |
3
|
ad2antrr |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> C e. ( Met ` X ) ) |
19 |
|
metcl |
|- ( ( C e. ( Met ` X ) /\ x e. X /\ y e. X ) -> ( x C y ) e. RR ) |
20 |
18 8 9 19
|
syl3anc |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( x C y ) e. RR ) |
21 |
14
|
rpred |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> R e. RR ) |
22 |
21 11
|
remulcld |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( R x. ( x D y ) ) e. RR ) |
23 |
|
lelttr |
|- ( ( ( x C y ) e. RR /\ ( R x. ( x D y ) ) e. RR /\ S e. RR ) -> ( ( ( x C y ) <_ ( R x. ( x D y ) ) /\ ( R x. ( x D y ) ) < S ) -> ( x C y ) < S ) ) |
24 |
20 22 13 23
|
syl3anc |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( ( ( x C y ) <_ ( R x. ( x D y ) ) /\ ( R x. ( x D y ) ) < S ) -> ( x C y ) < S ) ) |
25 |
17 24
|
mpand |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( ( R x. ( x D y ) ) < S -> ( x C y ) < S ) ) |
26 |
15 25
|
sylbird |
|- ( ( ( ph /\ ( x e. X /\ S e. RR+ ) ) /\ y e. X ) -> ( ( x D y ) < ( S / R ) -> ( x C y ) < S ) ) |
27 |
26
|
ss2rabdv |
|- ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> { y e. X | ( x D y ) < ( S / R ) } C_ { y e. X | ( x C y ) < S } ) |
28 |
|
metxmet |
|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) ) |
29 |
4 28
|
syl |
|- ( ph -> D e. ( *Met ` X ) ) |
30 |
29
|
adantr |
|- ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> D e. ( *Met ` X ) ) |
31 |
|
simprl |
|- ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> x e. X ) |
32 |
|
simpr |
|- ( ( x e. X /\ S e. RR+ ) -> S e. RR+ ) |
33 |
|
rpdivcl |
|- ( ( S e. RR+ /\ R e. RR+ ) -> ( S / R ) e. RR+ ) |
34 |
32 5 33
|
syl2anr |
|- ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> ( S / R ) e. RR+ ) |
35 |
34
|
rpxrd |
|- ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> ( S / R ) e. RR* ) |
36 |
|
blval |
|- ( ( D e. ( *Met ` X ) /\ x e. X /\ ( S / R ) e. RR* ) -> ( x ( ball ` D ) ( S / R ) ) = { y e. X | ( x D y ) < ( S / R ) } ) |
37 |
30 31 35 36
|
syl3anc |
|- ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> ( x ( ball ` D ) ( S / R ) ) = { y e. X | ( x D y ) < ( S / R ) } ) |
38 |
|
metxmet |
|- ( C e. ( Met ` X ) -> C e. ( *Met ` X ) ) |
39 |
3 38
|
syl |
|- ( ph -> C e. ( *Met ` X ) ) |
40 |
39
|
adantr |
|- ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> C e. ( *Met ` X ) ) |
41 |
|
rpxr |
|- ( S e. RR+ -> S e. RR* ) |
42 |
41
|
ad2antll |
|- ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> S e. RR* ) |
43 |
|
blval |
|- ( ( C e. ( *Met ` X ) /\ x e. X /\ S e. RR* ) -> ( x ( ball ` C ) S ) = { y e. X | ( x C y ) < S } ) |
44 |
40 31 42 43
|
syl3anc |
|- ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> ( x ( ball ` C ) S ) = { y e. X | ( x C y ) < S } ) |
45 |
27 37 44
|
3sstr4d |
|- ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> ( x ( ball ` D ) ( S / R ) ) C_ ( x ( ball ` C ) S ) ) |