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