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

Metamath Proof Explorer

Theorem metdcn

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
metdcn.2 ⊢ K = TopOpen ⁡ ℂ fld
Assertion metdcn ⊢ D ∈ Met ⁡ X → D ∈ J × t J Cn K

Proof

Step Hyp Ref Expression
1 xmetdcn2.1 ⊢ J = MetOpen ⁡ D
2 metdcn.2 ⊢ K = TopOpen ⁡ ℂ fld
3 2 tgioo2 ⊢ topGen ⁡ ran ⁡ . = K ↾ 𝑡 ℝ
4 3 oveq2i ⊢ J × t J Cn topGen ⁡ ran ⁡ . = J × t J Cn K ↾ 𝑡 ℝ
5 2 cnfldtop ⊢ K ∈ Top
6 cnrest2r ⊢ K ∈ Top → J × t J Cn K ↾ 𝑡 ℝ ⊆ J × t J Cn K
7 5 6 ax-mp ⊢ J × t J Cn K ↾ 𝑡 ℝ ⊆ J × t J Cn K
8 4 7 eqsstri ⊢ J × t J Cn topGen ⁡ ran ⁡ . ⊆ J × t J Cn K
9 eqid ⊢ topGen ⁡ ran ⁡ . = topGen ⁡ ran ⁡ .
10 1 9 metdcn2 ⊢ D ∈ Met ⁡ X → D ∈ J × t J Cn topGen ⁡ ran ⁡ .
11 8 10 sselid ⊢ D ∈ Met ⁡ X → D ∈ J × t J Cn K