Definition df-mopn

Description: Define a function whose value is the family of open sets of a metric space. See elmopn for its main property. (Contributed by NM, 1-Sep-2006)

	Ref	Expression
Assertion	df-mopn	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmopn	|- MetOpen
1		vd	|- d
2		cxmet	|- *Met
3	2	crn	|- ran *Met
4	3	cuni	|- U. ran *Met
5		ctg	|- topGen
6		cbl	|- ball
7	1	cv	|- d
8	7 6	cfv	|- ( ball ` d )
9	8	crn	|- ran ( ball ` d )
10	9 5	cfv	|- ( topGen ` ran ( ball ` d ) )
11	1 4 10	cmpt	|- ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
12	0 11	wceq	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )