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

Metamath Proof Explorer

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