Step |
Hyp |
Ref |
Expression |
1 |
|
ssrab2 |
|- { y e. X | ( x D y ) < r } C_ X |
2 |
|
elfvdm |
|- ( D e. ( PsMet ` X ) -> X e. dom PsMet ) |
3 |
|
elpw2g |
|- ( X e. dom PsMet -> ( { y e. X | ( x D y ) < r } e. ~P X <-> { y e. X | ( x D y ) < r } C_ X ) ) |
4 |
2 3
|
syl |
|- ( D e. ( PsMet ` X ) -> ( { y e. X | ( x D y ) < r } e. ~P X <-> { y e. X | ( x D y ) < r } C_ X ) ) |
5 |
1 4
|
mpbiri |
|- ( D e. ( PsMet ` X ) -> { y e. X | ( x D y ) < r } e. ~P X ) |
6 |
5
|
a1d |
|- ( D e. ( PsMet ` X ) -> ( ( x e. X /\ r e. RR* ) -> { y e. X | ( x D y ) < r } e. ~P X ) ) |
7 |
6
|
ralrimivv |
|- ( D e. ( PsMet ` X ) -> A. x e. X A. r e. RR* { y e. X | ( x D y ) < r } e. ~P X ) |
8 |
|
eqid |
|- ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) = ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) |
9 |
8
|
fmpo |
|- ( A. x e. X A. r e. RR* { y e. X | ( x D y ) < r } e. ~P X <-> ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) : ( X X. RR* ) --> ~P X ) |
10 |
7 9
|
sylib |
|- ( D e. ( PsMet ` X ) -> ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) : ( X X. RR* ) --> ~P X ) |
11 |
|
blfvalps |
|- ( D e. ( PsMet ` X ) -> ( ball ` D ) = ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) ) |
12 |
11
|
feq1d |
|- ( D e. ( PsMet ` X ) -> ( ( ball ` D ) : ( X X. RR* ) --> ~P X <-> ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) : ( X X. RR* ) --> ~P X ) ) |
13 |
10 12
|
mpbird |
|- ( D e. ( PsMet ` X ) -> ( ball ` D ) : ( X X. RR* ) --> ~P X ) |