tmslem

	Ref	Expression
Hypotheses	tmsval.m	$⊢ M = \{⟨{Base}_{ndx}, X⟩, ⟨dist (ndx), D⟩\}$
	tmsval.k	$⊢ K = toMetSp (D)$
Assertion	tmslem	$⊢ D \in ∞Met (X) \to (X = {Base}_{K} \land D = dist (K) \land MetOpen (D) = TopOpen (K))$

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

Metamath Proof Explorer