This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem blf

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

Ref Expression
Assertion blf 
|- ( D e. ( *Met ` 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. ( *Met ` X ) -> X e. dom *Met )
3 elpw2g 
 |-  ( X e. dom *Met -> ( { 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. ( *Met ` 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. ( *Met ` X ) -> { y e. X | ( x D y ) < r } e. ~P X )
6 5 a1d 
 |-  ( D e. ( *Met ` X ) -> ( ( x e. X /\ r e. RR* ) -> { y e. X | ( x D y ) < r } e. ~P X ) )
7 6 ralrimivv 
 |-  ( D e. ( *Met ` 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. ( *Met ` X ) -> ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) : ( X X. RR* ) --> ~P X )
11 blfval 
 |-  ( D e. ( *Met ` X ) -> ( ball ` D ) = ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) )
12 11 feq1d 
 |-  ( D e. ( *Met ` 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. ( *Met ` X ) -> ( ball ` D ) : ( X X. RR* ) --> ~P X )