Metamath Proof Explorer


Theorem metdcn

Description: The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses xmetdcn2.1 𝐽 = ( MetOpen ‘ 𝐷 )
metdcn.2 𝐾 = ( TopOpen ‘ ℂfld )
Assertion metdcn ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 xmetdcn2.1 𝐽 = ( MetOpen ‘ 𝐷 )
2 metdcn.2 𝐾 = ( TopOpen ‘ ℂfld )
3 2 tgioo2 ( topGen ‘ ran (,) ) = ( 𝐾t ℝ )
4 3 oveq2i ( ( 𝐽 ×t 𝐽 ) Cn ( topGen ‘ ran (,) ) ) = ( ( 𝐽 ×t 𝐽 ) Cn ( 𝐾t ℝ ) )
5 2 cnfldtop 𝐾 ∈ Top
6 cnrest2r ( 𝐾 ∈ Top → ( ( 𝐽 ×t 𝐽 ) Cn ( 𝐾t ℝ ) ) ⊆ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
7 5 6 ax-mp ( ( 𝐽 ×t 𝐽 ) Cn ( 𝐾t ℝ ) ) ⊆ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 )
8 4 7 eqsstri ( ( 𝐽 ×t 𝐽 ) Cn ( topGen ‘ ran (,) ) ) ⊆ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 )
9 eqid ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
10 1 9 metdcn2 ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( topGen ‘ ran (,) ) ) )
11 8 10 sselid ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )