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	$$⊢\mathrm{MetOpen}=\left(d\in \bigcup \mathrm{ran}\mathrm{\infty Met}⟼\mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(d\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmopn	$$class\mathrm{MetOpen}$$
1		vd	$$setvard$$
2		cxmet	$$class\mathrm{\infty Met}$$
3	2	crn	$$class\mathrm{ran}\mathrm{\infty Met}$$
4	3	cuni	$$class\bigcup \mathrm{ran}\mathrm{\infty Met}$$
5		ctg	$$class\mathrm{topGen}$$
6		cbl	$$class\mathrm{ball}$$
7	1	cv	$$setvard$$
8	7 6	cfv	$$class\mathrm{ball}\left(d\right)$$
9	8	crn	$$class\mathrm{ran}\mathrm{ball}\left(d\right)$$
10	9 5	cfv	$$class\mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(d\right)\right)$$
11	1 4 10	cmpt	$$class\left(d\in \bigcup \mathrm{ran}\mathrm{\infty Met}⟼\mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(d\right)\right)\right)$$
12	0 11	wceq	$$wff\mathrm{MetOpen}=\left(d\in \bigcup \mathrm{ran}\mathrm{\infty Met}⟼\mathrm{topGen}\left(\mathrm{ran}\mathrm{ball}\left(d\right)\right)\right)$$