Step |
Hyp |
Ref |
Expression |
1 |
|
simp2 |
|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ ( R e. RR* /\ 0 < R ) ) -> P e. X ) |
2 |
|
psmet0 |
|- ( ( D e. ( PsMet ` X ) /\ P e. X ) -> ( P D P ) = 0 ) |
3 |
2
|
3adant3 |
|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ ( R e. RR* /\ 0 < R ) ) -> ( P D P ) = 0 ) |
4 |
|
simp3r |
|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ ( R e. RR* /\ 0 < R ) ) -> 0 < R ) |
5 |
3 4
|
eqbrtrd |
|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ ( R e. RR* /\ 0 < R ) ) -> ( P D P ) < R ) |
6 |
|
elblps |
|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( P e. ( P ( ball ` D ) R ) <-> ( P e. X /\ ( P D P ) < R ) ) ) |
7 |
6
|
3adant3r |
|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ ( R e. RR* /\ 0 < R ) ) -> ( P e. ( P ( ball ` D ) R ) <-> ( P e. X /\ ( P D P ) < R ) ) ) |
8 |
1 5 7
|
mpbir2and |
|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ ( R e. RR* /\ 0 < R ) ) -> P e. ( P ( ball ` D ) R ) ) |