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

Metamath Proof Explorer

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 sselid ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )