This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑑 ) ⟩ ) )