Step |
Hyp |
Ref |
Expression |
1 |
|
blss |
|- ( ( D e. ( *Met ` X ) /\ x e. ran ( ball ` D ) /\ P e. x ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ x ) |
2 |
|
sstr |
|- ( ( ( P ( ball ` D ) r ) C_ x /\ x C_ A ) -> ( P ( ball ` D ) r ) C_ A ) |
3 |
2
|
expcom |
|- ( x C_ A -> ( ( P ( ball ` D ) r ) C_ x -> ( P ( ball ` D ) r ) C_ A ) ) |
4 |
3
|
reximdv |
|- ( x C_ A -> ( E. r e. RR+ ( P ( ball ` D ) r ) C_ x -> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) ) |
5 |
1 4
|
syl5com |
|- ( ( D e. ( *Met ` X ) /\ x e. ran ( ball ` D ) /\ P e. x ) -> ( x C_ A -> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) ) |
6 |
5
|
3expa |
|- ( ( ( D e. ( *Met ` X ) /\ x e. ran ( ball ` D ) ) /\ P e. x ) -> ( x C_ A -> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) ) |
7 |
6
|
expimpd |
|- ( ( D e. ( *Met ` X ) /\ x e. ran ( ball ` D ) ) -> ( ( P e. x /\ x C_ A ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) ) |
8 |
7
|
adantlr |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ x e. ran ( ball ` D ) ) -> ( ( P e. x /\ x C_ A ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) ) |
9 |
8
|
rexlimdva |
|- ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) ) |
10 |
|
simpll |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> D e. ( *Met ` X ) ) |
11 |
|
simplr |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> P e. X ) |
12 |
|
rpxr |
|- ( r e. RR+ -> r e. RR* ) |
13 |
12
|
ad2antrl |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> r e. RR* ) |
14 |
|
blelrn |
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ r e. RR* ) -> ( P ( ball ` D ) r ) e. ran ( ball ` D ) ) |
15 |
10 11 13 14
|
syl3anc |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> ( P ( ball ` D ) r ) e. ran ( ball ` D ) ) |
16 |
|
simprl |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> r e. RR+ ) |
17 |
|
blcntr |
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ r e. RR+ ) -> P e. ( P ( ball ` D ) r ) ) |
18 |
10 11 16 17
|
syl3anc |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> P e. ( P ( ball ` D ) r ) ) |
19 |
|
simprr |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> ( P ( ball ` D ) r ) C_ A ) |
20 |
|
eleq2 |
|- ( x = ( P ( ball ` D ) r ) -> ( P e. x <-> P e. ( P ( ball ` D ) r ) ) ) |
21 |
|
sseq1 |
|- ( x = ( P ( ball ` D ) r ) -> ( x C_ A <-> ( P ( ball ` D ) r ) C_ A ) ) |
22 |
20 21
|
anbi12d |
|- ( x = ( P ( ball ` D ) r ) -> ( ( P e. x /\ x C_ A ) <-> ( P e. ( P ( ball ` D ) r ) /\ ( P ( ball ` D ) r ) C_ A ) ) ) |
23 |
22
|
rspcev |
|- ( ( ( P ( ball ` D ) r ) e. ran ( ball ` D ) /\ ( P e. ( P ( ball ` D ) r ) /\ ( P ( ball ` D ) r ) C_ A ) ) -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) ) |
24 |
15 18 19 23
|
syl12anc |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( r e. RR+ /\ ( P ( ball ` D ) r ) C_ A ) ) -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) ) |
25 |
24
|
rexlimdvaa |
|- ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( E. r e. RR+ ( P ( ball ` D ) r ) C_ A -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) ) ) |
26 |
9 25
|
impbid |
|- ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) <-> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) ) |