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	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion	mopnval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mopnval.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		fvssunirn	⊢ ( ∞Met ‘ 𝑋 ) ⊆ ∪ ran ∞Met
3	2	sseli	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ∪ ran ∞Met )
4		fveq2	⊢ ( 𝑑 = 𝐷 → ( ball ‘ 𝑑 ) = ( ball ‘ 𝐷 ) )
5	4	rneqd	⊢ ( 𝑑 = 𝐷 → ran ( ball ‘ 𝑑 ) = ran ( ball ‘ 𝐷 ) )
6	5	fveq2d	⊢ ( 𝑑 = 𝐷 → ( topGen ‘ ran ( ball ‘ 𝑑 ) ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
7		df-mopn	⊢ MetOpen = ( 𝑑 ∈ ∪ ran ∞Met ↦ ( topGen ‘ ran ( ball ‘ 𝑑 ) ) )
8		fvex	⊢ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ∈ V
9	6 7 8	fvmpt	⊢ ( 𝐷 ∈ ∪ ran ∞Met → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
10	1 9	syl5eq	⊢ ( 𝐷 ∈ ∪ ran ∞Met → 𝐽 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
11	3 10	syl	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )