Theorem tmslemOLD

Description: Obsolete version of tmslem as of 28-Oct-2024. Lemma for tmsbas , tmsds , and tmstopn . (Contributed by Mario Carneiro, 2-Sep-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	tmsval.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}$$
	tmsval.k	$$⊢K=\mathrm{toMetSp}\left(D\right)$$
Assertion	tmslemOLD	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(X={\mathrm{Base}}_K\wedge D=\mathrm{dist}\left(K\right)\wedge \mathrm{MetOpen}\left(D\right)=\mathrm{TopOpen}\left(K\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		tmsval.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}$$
2		tmsval.k	$$⊢K=\mathrm{toMetSp}\left(D\right)$$
3		elfvdm	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to X\in \mathrm{dom}\mathrm{\infty Met}$$
4		df-ds	$$⊢\mathrm{dist}=\mathrm{Slot}12$$
5		1nn	$$⊢1\in \mathbb{N}$$
6		2nn0	$$⊢2\in {\mathbb{N}}_0$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8		1lt10	$$⊢1<10$$
9	5 6 7 8	declti	$$⊢1<12$$
10		2nn	$$⊢2\in \mathbb{N}$$
11	7 10	decnncl	$$⊢12\in \mathbb{N}$$
12	1 4 9 11	2strbas	$$⊢X\in \mathrm{dom}\mathrm{\infty Met}\to X={\mathrm{Base}}_M$$
13	3 12	syl	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to X={\mathrm{Base}}_M$$
14		xmetf	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D:X\times X⟶{ℝ}^{*}$$
15		ffn	$$⊢D:X\times X⟶{ℝ}^{*}\to DFn\left(X\times X\right)$$
16		fnresdm	$$⊢DFn\left(X\times X\right)\to {D\upharpoonright }_{\left(X\times X\right)}=D$$
17	14 15 16	3syl	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to {D\upharpoonright }_{\left(X\times X\right)}=D$$
18	1 4 9 11	2strop	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D=\mathrm{dist}\left(M\right)$$
19	18	reseq1d	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to {D\upharpoonright }_{\left(X\times X\right)}={\mathrm{dist}\left(M\right)\upharpoonright }_{\left(X\times X\right)}$$
20	17 19	eqtr3d	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D={\mathrm{dist}\left(M\right)\upharpoonright }_{\left(X\times X\right)}$$
21	1 2	tmsval	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to K=M\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(D\right)⟩$$
22	13 20 21	setsmsbas	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to X={\mathrm{Base}}_K$$
23	13 20 21	setsmsds	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{dist}\left(M\right)=\mathrm{dist}\left(K\right)$$
24	18 23	eqtrd	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D=\mathrm{dist}\left(K\right)$$
25		prex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}\in \mathrm{V}$$
26	1 25	eqeltri	$$⊢M\in \mathrm{V}$$
27	26	a1i	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to M\in \mathrm{V}$$
28	13 20 21 27	setsmstopn	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{MetOpen}\left(D\right)=\mathrm{TopOpen}\left(K\right)$$
29	22 24 28	3jca	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(X={\mathrm{Base}}_K\wedge D=\mathrm{dist}\left(K\right)\wedge \mathrm{MetOpen}\left(D\right)=\mathrm{TopOpen}\left(K\right)\right)$$