Definition 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 = ( 𝑑 ∈ ∪ ran ∞Met ↦ ( { ⟨ ( Base ‘ ndx ) , dom dom 𝑑 ⟩ , ⟨ ( dist ‘ ndx ) , 𝑑 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝑑 ) ⟩ ) )

Detailed syntax breakdown

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