Theorem xmetdcn

Description: The metric function of an extended metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 4-Sep-2015)

	Ref	Expression
Hypotheses	xmetdcn2.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	xmetdcn.2	⊢ 𝐾 = ( ordTop ‘ ≤ )
Assertion	xmetdcn	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		xmetdcn2.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		xmetdcn.2	⊢ 𝐾 = ( ordTop ‘ ≤ )
3		letopon	⊢ ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* )
4	2 3	eqeltri	⊢ 𝐾 ∈ ( TopOn ‘ ℝ* )
5		eqid	⊢ ( dist ‘ ℝ*𝑠 ) = ( dist ‘ ℝ*𝑠 )
6		eqid	⊢ ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) = ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) )
7	5 6	xrsmopn	⊢ ( ordTop ‘ ≤ ) ⊆ ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) )
8	2 7	eqsstri	⊢ 𝐾 ⊆ ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) )
9	5	xrsxmet	⊢ ( dist ‘ ℝ*𝑠 ) ∈ ( ∞Met ‘ ℝ* )
10	6	mopnuni	⊢ ( ( dist ‘ ℝ*𝑠 ) ∈ ( ∞Met ‘ ℝ* ) → ℝ* = ∪ ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) )
11	9 10	ax-mp	⊢ ℝ* = ∪ ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) )
12	11	cnss2	⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℝ* ) ∧ 𝐾 ⊆ ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) → ( ( 𝐽 ×t 𝐽 ) Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) ⊆ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
13	4 8 12	mp2an	⊢ ( ( 𝐽 ×t 𝐽 ) Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) ⊆ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 )
14	1 5 6	xmetdcn2	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) )
15	13 14	sseldi	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )