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 )