Theorem blelrn

Description: A ball belongs to the set of balls of a metric space. (Contributed by NM, 2-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

	Ref	Expression
Assertion	blelrn	|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) e. ran ( ball ` D ) )

Proof

Step	Hyp	Ref	Expression
1		blf	|- ( D e. ( *Met ` X ) -> ( ball ` D ) : ( X X. RR* ) --> ~P X )
2	1	ffnd	|- ( D e. ( *Met ` X ) -> ( ball ` D ) Fn ( X X. RR* ) )
3		fnovrn	|- ( ( ( ball ` D ) Fn ( X X. RR* ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) e. ran ( ball ` D ) )
4	2 3	syl3an1	|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) e. ran ( ball ` D ) )