Theorem setsmstset

Description: The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypotheses	setsms.x	$$⊢\phi \to X={\mathrm{Base}}_M$$
	setsms.d	$$⊢\phi \to D={\mathrm{dist}\left(M\right)\upharpoonright }_{\left(X\times X\right)}$$
	setsms.k	$$⊢\phi \to K=M\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(D\right)⟩$$
	setsms.m	$$⊢\phi \to M\in V$$
Assertion	setsmstset	$$⊢\phi \to \mathrm{MetOpen}\left(D\right)=\mathrm{TopSet}\left(K\right)$$

Proof

Step	Hyp	Ref	Expression
1		setsms.x	$$⊢\phi \to X={\mathrm{Base}}_M$$
2		setsms.d	$$⊢\phi \to D={\mathrm{dist}\left(M\right)\upharpoonright }_{\left(X\times X\right)}$$
3		setsms.k	$$⊢\phi \to K=M\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(D\right)⟩$$
4		setsms.m	$$⊢\phi \to M\in V$$
5		fvex	$$⊢\mathrm{MetOpen}\left(D\right)\in \mathrm{V}$$
6		tsetid	$$⊢\mathrm{TopSet}=\mathrm{Slot}\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
7	6	setsid	$$⊢\left(M\in V\wedge \mathrm{MetOpen}\left(D\right)\in \mathrm{V}\right)\to \mathrm{MetOpen}\left(D\right)=\mathrm{TopSet}\left(M\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(D\right)⟩\right)$$
8	4 5 7	sylancl	$$⊢\phi \to \mathrm{MetOpen}\left(D\right)=\mathrm{TopSet}\left(M\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(D\right)⟩\right)$$
9	3	fveq2d	$$⊢\phi \to \mathrm{TopSet}\left(K\right)=\mathrm{TopSet}\left(M\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(D\right)⟩\right)$$
10	8 9	eqtr4d	$$⊢\phi \to \mathrm{MetOpen}\left(D\right)=\mathrm{TopSet}\left(K\right)$$