Step |
Hyp |
Ref |
Expression |
1 |
|
0xr |
|- 0 e. RR* |
2 |
1
|
a1i |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> 0 e. RR* ) |
3 |
|
simpl1 |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> D e. ( *Met ` X ) ) |
4 |
|
simpl2 |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> P e. X ) |
5 |
|
elbl |
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A e. X /\ ( P D A ) < R ) ) ) |
6 |
5
|
simprbda |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> A e. X ) |
7 |
|
xmetcl |
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. X ) -> ( P D A ) e. RR* ) |
8 |
3 4 6 7
|
syl3anc |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> ( P D A ) e. RR* ) |
9 |
|
simpl3 |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> R e. RR* ) |
10 |
|
xmetge0 |
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. X ) -> 0 <_ ( P D A ) ) |
11 |
3 4 6 10
|
syl3anc |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> 0 <_ ( P D A ) ) |
12 |
5
|
simplbda |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> ( P D A ) < R ) |
13 |
2 8 9 11 12
|
xrlelttrd |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> 0 < R ) |