Theorem msdcn

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, 5-Oct-2015)

	Ref	Expression
Hypotheses	msdcn.x	⊢ 𝑋 = ( Base ‘ 𝑀 )
	msdcn.d	⊢ 𝐷 = ( dist ‘ 𝑀 )
	msdcn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑀 )
	msdcn.2	⊢ 𝐾 = ( topGen ‘ ran (,) )
Assertion	msdcn	⊢ ( 𝑀 ∈ MetSp → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		msdcn.x	⊢ 𝑋 = ( Base ‘ 𝑀 )
2		msdcn.d	⊢ 𝐷 = ( dist ‘ 𝑀 )
3		msdcn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑀 )
4		msdcn.2	⊢ 𝐾 = ( topGen ‘ ran (,) )
5	1 2	msmet2	⊢ ( 𝑀 ∈ MetSp → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) )
6		eqid	⊢ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) )
7	6 4	metdcn2	⊢ ( ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ×t ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ) Cn 𝐾 ) )
8	5 7	syl	⊢ ( 𝑀 ∈ MetSp → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ×t ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ) Cn 𝐾 ) )
9	2	reseq1i	⊢ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) )
10	3 1 9	mstopn	⊢ ( 𝑀 ∈ MetSp → 𝐽 = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) )
11	10 10	oveq12d	⊢ ( 𝑀 ∈ MetSp → ( 𝐽 ×t 𝐽 ) = ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ×t ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ) )
12	11	oveq1d	⊢ ( 𝑀 ∈ MetSp → ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) = ( ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ×t ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ) Cn 𝐾 ) )
13	8 12	eleqtrrd	⊢ ( 𝑀 ∈ MetSp → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )