Theorem setsmsds

Description: The distance function 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)⟩$$
Assertion	setsmsds	$$⊢\phi \to \mathrm{dist}\left(M\right)=\mathrm{dist}\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	3	fveq2d	$$⊢\phi \to \mathrm{dist}\left(K\right)=\mathrm{dist}\left(M\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(D\right)⟩\right)$$
5		dsid	$$⊢\mathrm{dist}=\mathrm{Slot}\mathrm{dist}\left(\mathrm{ndx}\right)$$
6		9re	$$⊢9\in ℝ$$
7		1nn	$$⊢1\in \mathbb{N}$$
8		2nn0	$$⊢2\in {\mathbb{N}}_0$$
9		9nn0	$$⊢9\in {\mathbb{N}}_0$$
10		9lt10	$$⊢9<10$$
11	7 8 9 10	declti	$$⊢9<12$$
12	6 11	gtneii	$$⊢12\ne 9$$
13		dsndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)=12$$
14		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
15	13 14	neeq12i	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\leftrightarrow 12\ne 9$$
16	12 15	mpbir	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
17	5 16	setsnid	$$⊢\mathrm{dist}\left(M\right)=\mathrm{dist}\left(M\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(D\right)⟩\right)$$
18	4 17	syl6reqr	$$⊢\phi \to \mathrm{dist}\left(M\right)=\mathrm{dist}\left(K\right)$$