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

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 𝐾 ) )