Theorem mopnval

Description: An open set is a subset of a metric space which includes a ball around each of its points. Definition 1.3-2 of Kreyszig p. 18. The object ( MetOpenD ) is the family of all open sets in the metric space determined by the metric D . By mopntop , the open sets of a metric space form a topology J , whose base set is U. J by mopnuni . (Contributed by NM, 1-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		mopnval.1	|- J = ( MetOpen ` D )
2		fvssunirn	|- ( *Met ` X ) C_ U. ran *Met
3	2	sseli	|- ( D e. ( *Met ` X ) -> D e. U. ran *Met )
4		fveq2	|- ( d = D -> ( ball ` d ) = ( ball ` D ) )
5	4	rneqd	|- ( d = D -> ran ( ball ` d ) = ran ( ball ` D ) )
6	5	fveq2d	|- ( d = D -> ( topGen ` ran ( ball ` d ) ) = ( topGen ` ran ( ball ` D ) ) )
7		df-mopn	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
8		fvex	|- ( topGen ` ran ( ball ` D ) ) e. _V
9	6 7 8	fvmpt	|- ( D e. U. ran *Met -> ( MetOpen ` D ) = ( topGen ` ran ( ball ` D ) ) )
10	1 9	syl5eq	|- ( D e. U. ran *Met -> J = ( topGen ` ran ( ball ` D ) ) )
11	3 10	syl	|- ( D e. ( *Met ` X ) -> J = ( topGen ` ran ( ball ` D ) ) )