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 ⊢ J = MetOpen ⁡ D
metdcn2.2 ⊢ K = topGen ⁡ ran ⁡ .
Assertion metdcn2 ⊢ D ∈ Met ⁡ X → D ∈ J × t J Cn K

Proof

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