Theorem metdcn2

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 ‘ 𝐷 )
	metdcn2.2	⊢ 𝐾 = ( topGen ‘ ran (,) )
Assertion	metdcn2	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		xmetdcn2.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		metdcn2.2	⊢ 𝐾 = ( topGen ‘ ran (,) )
3		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4		eqid	⊢ ( ordTop ‘ ≤ ) = ( ordTop ‘ ≤ )
5	1 4	xmetdcn	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( ordTop ‘ ≤ ) ) )
6	3 5	syl	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( ordTop ‘ ≤ ) ) )
7		letopon	⊢ ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* )
8		metf	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
9	8	frnd	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → ran 𝐷 ⊆ ℝ )
10		ressxr	⊢ ℝ ⊆ ℝ*
11	10	a1i	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → ℝ ⊆ ℝ* )
12		cnrest2	⊢ ( ( ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* ) ∧ ran 𝐷 ⊆ ℝ ∧ ℝ ⊆ ℝ* ) → ( 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( ordTop ‘ ≤ ) ) ↔ 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( ( ordTop ‘ ≤ ) ↾t ℝ ) ) ) )
13	7 9 11 12	mp3an2i	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → ( 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( ordTop ‘ ≤ ) ) ↔ 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( ( ordTop ‘ ≤ ) ↾t ℝ ) ) ) )
14	6 13	mpbid	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( ( ordTop ‘ ≤ ) ↾t ℝ ) ) )
15		eqid	⊢ ( ( ordTop ‘ ≤ ) ↾t ℝ ) = ( ( ordTop ‘ ≤ ) ↾t ℝ )
16	15	xrtgioo	⊢ ( topGen ‘ ran (,) ) = ( ( ordTop ‘ ≤ ) ↾t ℝ )
17	2 16	eqtri	⊢ 𝐾 = ( ( ordTop ‘ ≤ ) ↾t ℝ )
18	17	oveq2i	⊢ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) = ( ( 𝐽 ×t 𝐽 ) Cn ( ( ordTop ‘ ≤ ) ↾t ℝ ) )
19	14 18	eleqtrrdi	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )