Theorem blopn

Description: A ball of a metric space is an open set. (Contributed by NM, 9-Mar-2007) (Revised by Mario Carneiro, 12-Nov-2013)

	Ref	Expression
Hypothesis	mopni.1	|- J = ( MetOpen ` D )
Assertion	blopn	|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) e. J )

Proof

Step	Hyp	Ref	Expression
1		mopni.1	|- J = ( MetOpen ` D )
2	1	blssopn	|- ( D e. ( *Met ` X ) -> ran ( ball ` D ) C_ J )
3	2	3ad2ant1	|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ran ( ball ` D ) C_ J )
4		blelrn	|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) e. ran ( ball ` D ) )
5	3 4	sseldd	|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) e. J )