df-tms

Description: Define the function mapping a metric to the metric space which it defines. (Contributed by Mario Carneiro, 2-Sep-2015)

		Ref	Expression
	Assertion	df-tms	$⊢ toMetSp = (d \in ⋃ ran ∞Met ⟼ \{⟨{Base}_{ndx}, dom dom d⟩, ⟨dist (ndx), d⟩\} sSet ⟨TopSet (ndx), MetOpen (d)⟩)$

Step	Hyp	Ref	Expression
0		ctms	$class toMetSp$
1		vd	$setvar d$
2		cxmet	$class ∞Met$
3	2	crn	$class ran ∞Met$
4	3	cuni	$class ⋃ ran ∞Met$
5		cbs	$class Base$
6		cnx	$class ndx$
7	6 5	cfv	$class {Base}_{ndx}$
8	1	cv	$setvar d$
9	8	cdm	$class dom d$
10	9	cdm	$class dom dom d$
11	7 10	cop	$class ⟨{Base}_{ndx}, dom dom d⟩$
12		cds	$class dist$
13	6 12	cfv	$class dist (ndx)$
14	13 8	cop	$class ⟨dist (ndx), d⟩$
15	11 14	cpr	$class \{⟨{Base}_{ndx}, dom dom d⟩, ⟨dist (ndx), d⟩\}$
16		csts	$class sSet$
17		cts	$class TopSet$
18	6 17	cfv	$class TopSet (ndx)$
19		cmopn	$class MetOpen$
20	8 19	cfv	$class MetOpen (d)$
21	18 20	cop	$class ⟨TopSet (ndx), MetOpen (d)⟩$
22	15 21 16	co	$class (\{⟨{Base}_{ndx}, dom dom d⟩, ⟨dist (ndx), d⟩\} sSet ⟨TopSet (ndx), MetOpen (d)⟩)$
23	1 4 22	cmpt	$class (d \in ⋃ ran ∞Met ⟼ \{⟨{Base}_{ndx}, dom dom d⟩, ⟨dist (ndx), d⟩\} sSet ⟨TopSet (ndx), MetOpen (d)⟩)$
24	0 23	wceq	$wff toMetSp = (d \in ⋃ ran ∞Met ⟼ \{⟨{Base}_{ndx}, dom dom d⟩, ⟨dist (ndx), d⟩\} sSet ⟨TopSet (ndx), MetOpen (d)⟩)$

Metamath Proof Explorer