tmsval

Description: For any metric there is an associated metric space. (Contributed by Mario Carneiro, 2-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		tmsval.m	$⊢ M = \{⟨{Base}_{ndx}, X⟩, ⟨dist (ndx), D⟩\}$
2		tmsval.k	$⊢ K = toMetSp (D)$
3		df-tms	$⊢ toMetSp = (d \in ⋃ ran ∞Met ⟼ \{⟨{Base}_{ndx}, dom dom d⟩, ⟨dist (ndx), d⟩\} sSet ⟨TopSet (ndx), MetOpen (d)⟩)$
4		dmeq	$⊢ d = D \to dom d = dom D$
5	4	dmeqd	$⊢ d = D \to dom dom d = dom dom D$
6		xmetf	$⊢ D \in ∞Met (X) \to D : X \times X ⟶ ℝ^{*}$
7	6	fdmd	$⊢ D \in ∞Met (X) \to dom D = X \times X$
8	7	dmeqd	$⊢ D \in ∞Met (X) \to dom dom D = dom (X \times X)$
9		dmxpid	$⊢ dom (X \times X) = X$
10	8 9	eqtrdi	$⊢ D \in ∞Met (X) \to dom dom D = X$
11	5 10	sylan9eqr	$⊢ (D \in ∞Met (X) \land d = D) \to dom dom d = X$
12	11	opeq2d	$⊢ (D \in ∞Met (X) \land d = D) \to ⟨{Base}_{ndx}, dom dom d⟩ = ⟨{Base}_{ndx}, X⟩$
13		simpr	$⊢ (D \in ∞Met (X) \land d = D) \to d = D$
14	13	opeq2d	$⊢ (D \in ∞Met (X) \land d = D) \to ⟨dist (ndx), d⟩ = ⟨dist (ndx), D⟩$
15	12 14	preq12d	$⊢ (D \in ∞Met (X) \land d = D) \to \{⟨{Base}_{ndx}, dom dom d⟩, ⟨dist (ndx), d⟩\} = \{⟨{Base}_{ndx}, X⟩, ⟨dist (ndx), D⟩\}$
16	15 1	eqtr4di	$⊢ (D \in ∞Met (X) \land d = D) \to \{⟨{Base}_{ndx}, dom dom d⟩, ⟨dist (ndx), d⟩\} = M$
17	13	fveq2d	$⊢ (D \in ∞Met (X) \land d = D) \to MetOpen (d) = MetOpen (D)$
18	17	opeq2d	$⊢ (D \in ∞Met (X) \land d = D) \to ⟨TopSet (ndx), MetOpen (d)⟩ = ⟨TopSet (ndx), MetOpen (D)⟩$
19	16 18	oveq12d	$⊢ (D \in ∞Met (X) \land d = D) \to \{⟨{Base}_{ndx}, dom dom d⟩, ⟨dist (ndx), d⟩\} sSet ⟨TopSet (ndx), MetOpen (d)⟩ = M sSet ⟨TopSet (ndx), MetOpen (D)⟩$
20		fvssunirn	$⊢ ∞Met (X) \subseteq ⋃ ran ∞Met$
21	20	sseli	$⊢ D \in ∞Met (X) \to D \in ⋃ ran ∞Met$
22		ovexd	$⊢ D \in ∞Met (X) \to M sSet ⟨TopSet (ndx), MetOpen (D)⟩ \in V$
23	3 19 21 22	fvmptd2	$⊢ D \in ∞Met (X) \to toMetSp (D) = M sSet ⟨TopSet (ndx), MetOpen (D)⟩$
24	2 23	syl5eq	$⊢ D \in ∞Met (X) \to K = M sSet ⟨TopSet (ndx), MetOpen (D)⟩$

Metamath Proof Explorer

Theorem tmsval

Proof