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 = ( 𝑑 ∈ ∪ ran ∞Met ↦ ( topGen ‘ ran ( ball ‘ 𝑑 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmopn	⊢ MetOpen
1		vd	⊢ 𝑑
2		cxmet	⊢ ∞Met
3	2	crn	⊢ ran ∞Met
4	3	cuni	⊢ ∪ ran ∞Met
5		ctg	⊢ topGen
6		cbl	⊢ ball
7	1	cv	⊢ 𝑑
8	7 6	cfv	⊢ ( ball ‘ 𝑑 )
9	8	crn	⊢ ran ( ball ‘ 𝑑 )
10	9 5	cfv	⊢ ( topGen ‘ ran ( ball ‘ 𝑑 ) )
11	1 4 10	cmpt	⊢ ( 𝑑 ∈ ∪ ran ∞Met ↦ ( topGen ‘ ran ( ball ‘ 𝑑 ) ) )
12	0 11	wceq	⊢ MetOpen = ( 𝑑 ∈ ∪ ran ∞Met ↦ ( topGen ‘ ran ( ball ‘ 𝑑 ) ) )