Step |
Hyp |
Ref |
Expression |
1 |
|
simpl1 |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> D e. ( PsMet ` X ) ) |
2 |
|
simpl2 |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> P e. X ) |
3 |
|
simpl3 |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> Q e. X ) |
4 |
|
simpr1 |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> R e. RR ) |
5 |
4
|
rexrd |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> R e. RR* ) |
6 |
|
simpr2 |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> S e. RR ) |
7 |
6
|
rexrd |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> S e. RR* ) |
8 |
6 4
|
resubcld |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( S - R ) e. RR ) |
9 |
|
simpr3 |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( P D Q ) <_ ( S - R ) ) |
10 |
|
psmetlecl |
|- ( ( D e. ( PsMet ` X ) /\ ( P e. X /\ Q e. X ) /\ ( ( S - R ) e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( P D Q ) e. RR ) |
11 |
1 2 3 8 9 10
|
syl122anc |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( P D Q ) e. RR ) |
12 |
|
rexsub |
|- ( ( S e. RR /\ R e. RR ) -> ( S +e -e R ) = ( S - R ) ) |
13 |
6 4 12
|
syl2anc |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( S +e -e R ) = ( S - R ) ) |
14 |
9 13
|
breqtrrd |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( P D Q ) <_ ( S +e -e R ) ) |
15 |
1 2 3 5 7 11 14
|
xblss2ps |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( P ( ball ` D ) R ) C_ ( Q ( ball ` D ) S ) ) |