Theorem blssopn

Description: The balls of a metric space are open sets. (Contributed by NM, 12-Sep-2006) (Revised by Mario Carneiro, 23-Dec-2013)

	Ref	Expression
Hypothesis	mopni.1	|- J = ( MetOpen ` D )
Assertion	blssopn	|- ( D e. ( *Met ` X ) -> ran ( ball ` D ) C_ J )

Proof

Step	Hyp	Ref	Expression
1		mopni.1	|- J = ( MetOpen ` D )
2		blbas	|- ( D e. ( *Met ` X ) -> ran ( ball ` D ) e. TopBases )
3		bastg	|- ( ran ( ball ` D ) e. TopBases -> ran ( ball ` D ) C_ ( topGen ` ran ( ball ` D ) ) )
4	2 3	syl	|- ( D e. ( *Met ` X ) -> ran ( ball ` D ) C_ ( topGen ` ran ( ball ` D ) ) )
5	1	mopnval	|- ( D e. ( *Met ` X ) -> J = ( topGen ` ran ( ball ` D ) ) )
6	4 5	sseqtrrd	|- ( D e. ( *Met ` X ) -> ran ( ball ` D ) C_ J )