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		basendxltdsndx	$⊢ {Base}_{ndx} < dist (ndx)$
5		dsndxnn	$⊢ dist (ndx) \in ℕ$
6	1 4 5	2strbas1	$⊢ X \in dom ∞Met \to X = {Base}_{M}$
7	3 6	syl	$⊢ D \in ∞Met (X) \to X = {Base}_{M}$
8		xmetf	$⊢ D \in ∞Met (X) \to D : X \times X ⟶ ℝ^{*}$
9		ffn	$⊢ D : X \times X ⟶ ℝ^{*} \to D Fn (X \times X)$
10		fnresdm	$⊢ D Fn (X \times X) \to {D ↾}_{(X \times X)} = D$
11	8 9 10	3syl	$⊢ D \in ∞Met (X) \to {D ↾}_{(X \times X)} = D$
12		dsid	$⊢ dist = Slot dist (ndx)$
13	1 4 5 12	2strop1	$⊢ D \in ∞Met (X) \to D = dist (M)$
14	13	reseq1d	$⊢ D \in ∞Met (X) \to {D ↾}_{(X \times X)} = {dist (M) ↾}_{(X \times X)}$
15	11 14	eqtr3d	$⊢ D \in ∞Met (X) \to D = {dist (M) ↾}_{(X \times X)}$
16	1 2	tmsval	$⊢ D \in ∞Met (X) \to K = M sSet ⟨TopSet (ndx), MetOpen (D)⟩$
17	7 15 16	setsmsbas	$⊢ D \in ∞Met (X) \to X = {Base}_{K}$
18	7 15 16	setsmsds	$⊢ D \in ∞Met (X) \to dist (M) = dist (K)$
19	13 18	eqtrd	$⊢ D \in ∞Met (X) \to D = dist (K)$
20		prex	$⊢ \{⟨{Base}_{ndx}, X⟩, ⟨dist (ndx), D⟩\} \in V$
21	1 20	eqeltri	$⊢ M \in V$
22	21	a1i	$⊢ D \in ∞Met (X) \to M \in V$
23	7 15 16 22	setsmstopn	$⊢ D \in ∞Met (X) \to MetOpen (D) = TopOpen (K)$
24	17 19 23	3jca	$⊢ D \in ∞Met (X) \to (X = {Base}_{K} \land D = dist (K) \land MetOpen (D) = TopOpen (K))$

Metamath Proof Explorer