# 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 )`