Metamath Proof Explorer


Theorem blfps

Description: Mapping of a ball. (Contributed by NM, 7-May-2007) (Revised by Mario Carneiro, 23-Aug-2015) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion blfps
|- ( D e. ( PsMet ` X ) -> ( ball ` D ) : ( X X. RR* ) --> ~P X )

Proof

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 )