Metamath Proof Explorer

Theorem tmsval

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

Ref Expression
Hypotheses tmsval.m ⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ }
tmsval.k ⊢ 𝐾 = ( toMetSp ‘ 𝐷 )
Assertion tmsval ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐾 = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 tmsval.m ⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ }
2 tmsval.k ⊢ 𝐾 = ( toMetSp ‘ 𝐷 )
3 df-tms ⊢ toMetSp = ( 𝑑 ∈ ∪ ran ∞Met ↦ ( { ⟨ ( Base ‘ ndx ) , dom dom 𝑑 ⟩ , ⟨ ( dist ‘ ndx ) , 𝑑 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝑑 ) ⟩ ) )
4 dmeq ⊢ ( 𝑑 = 𝐷 → dom 𝑑 = dom 𝐷 )
5 4 dmeqd ⊢ ( 𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷 )
6 xmetf ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
7 6 fdmd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
8 7 dmeqd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → dom dom 𝐷 = dom ( 𝑋 × 𝑋 ) )
9 dmxpid ⊢ dom ( 𝑋 × 𝑋 ) = 𝑋
10 8 9 eqtrdi ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → dom dom 𝐷 = 𝑋 )
11 5 10 sylan9eqr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom dom 𝑑 = 𝑋 )
12 11 opeq2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ⟨ ( Base ‘ ndx ) , dom dom 𝑑 ⟩ = ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ )
13 simpr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
14 13 opeq2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ⟨ ( dist ‘ ndx ) , 𝑑 ⟩ = ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ )
15 12 14 preq12d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → { ⟨ ( Base ‘ ndx ) , dom dom 𝑑 ⟩ , ⟨ ( dist ‘ ndx ) , 𝑑 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } )
16 15 1 eqtr4di ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → { ⟨ ( Base ‘ ndx ) , dom dom 𝑑 ⟩ , ⟨ ( dist ‘ ndx ) , 𝑑 ⟩ } = 𝑀 )
17 13 fveq2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( MetOpen ‘ 𝑑 ) = ( MetOpen ‘ 𝐷 ) )
18 17 opeq2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝑑 ) ⟩ = ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ )
19 16 18 oveq12d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( { ⟨ ( Base ‘ ndx ) , dom dom 𝑑 ⟩ , ⟨ ( dist ‘ ndx ) , 𝑑 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝑑 ) ⟩ ) = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )
20 fvssunirn ⊢ ( ∞Met ‘ 𝑋 ) ⊆ ∪ ran ∞Met
21 20 sseli ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ∪ ran ∞Met )
22 ovexd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) ∈ V )
23 3 19 21 22 fvmptd2 ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( toMetSp ‘ 𝐷 ) = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )
24 2 23 syl5eq ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐾 = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )