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=\mathrm{MetOpen}\left(D\right)$$
Assertion	mopnval	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to J=\mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(D\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mopnval.1	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
2		fvssunirn	$$⊢\mathrm{\infty Met}\left(X\right)\subseteq \bigcup \mathrm{ran}\mathrm{\infty Met}$$
3	2	sseli	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D\in \bigcup \mathrm{ran}\mathrm{\infty Met}$$
4		fveq2	$$⊢d=D\to \mathrm{ball}\left(d\right)=\mathrm{ball}\left(D\right)$$
5	4	rneqd	$$⊢d=D\to \mathrm{ran}\mathrm{ball}\left(d\right)=\mathrm{ran}\mathrm{ball}\left(D\right)$$
6	5	fveq2d	$$⊢d=D\to \mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(d\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(D\right)\right)$$
7		df-mopn	$$⊢\mathrm{MetOpen}=\left(d\in \bigcup \mathrm{ran}\mathrm{\infty Met}⟼\mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(d\right)\right)\right)$$
8		fvex	$$⊢\mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(D\right)\right)\in \mathrm{V}$$
9	6 7 8	fvmpt	$$⊢D\in \bigcup \mathrm{ran}\mathrm{\infty Met}\to \mathrm{MetOpen}\left(D\right)=\mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(D\right)\right)$$
10	1 9	syl5eq	$$⊢D\in \bigcup \mathrm{ran}\mathrm{\infty Met}\to J=\mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(D\right)\right)$$
11	3 10	syl	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to J=\mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(D\right)\right)$$