Theorem setsmsbas

Description: The base set 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	setsmsbas	$$⊢\phi \to X={\mathrm{Base}}_K$$

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		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
5		1re	$$⊢1\in ℝ$$
6		1lt9	$$⊢1<9$$
7	5 6	ltneii	$$⊢1\ne 9$$
8		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
9		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
10	8 9	neeq12i	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\leftrightarrow 1\ne 9$$
11	7 10	mpbir	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
12	4 11	setsnid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_{\left(M\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(D\right)⟩\right)}$$
13	3	fveq2d	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_{\left(M\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(D\right)⟩\right)}$$
14	12 1 13	3eqtr4a	$$⊢\phi \to X={\mathrm{Base}}_K$$