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 ⊢ J = MetOpen ⁡ D
xmetdcn.2 ⊢ K = ordTop ⁡ ≤
Assertion xmetdcn ⊢ D ∈ ∞Met ⁡ X → D ∈ J × t J Cn K

Proof

Step Hyp Ref Expression
1 xmetdcn2.1 ⊢ J = MetOpen ⁡ D
2 xmetdcn.2 ⊢ K = ordTop ⁡ ≤
3 letopon ⊢ ordTop ⁡ ≤ ∈ TopOn ⁡ ℝ *
4 2 3 eqeltri ⊢ K ∈ TopOn ⁡ ℝ *
5 eqid ⊢ dist ⁡ ℝ 𝑠 * = dist ⁡ ℝ 𝑠 *
6 eqid ⊢ MetOpen ⁡ dist ⁡ ℝ 𝑠 * = MetOpen ⁡ dist ⁡ ℝ 𝑠 *
7 5 6 xrsmopn ⊢ ordTop ⁡ ≤ ⊆ MetOpen ⁡ dist ⁡ ℝ 𝑠 *
8 2 7 eqsstri ⊢ K ⊆ MetOpen ⁡ dist ⁡ ℝ 𝑠 *
9 5 xrsxmet ⊢ dist ⁡ ℝ 𝑠 * ∈ ∞Met ⁡ ℝ *
10 6 mopnuni ⊢ dist ⁡ ℝ 𝑠 * ∈ ∞Met ⁡ ℝ * → ℝ * = ⋃ MetOpen ⁡ dist ⁡ ℝ 𝑠 *
11 9 10 ax-mp ⊢ ℝ * = ⋃ MetOpen ⁡ dist ⁡ ℝ 𝑠 *
12 11 cnss2 ⊢ K ∈ TopOn ⁡ ℝ * ∧ K ⊆ MetOpen ⁡ dist ⁡ ℝ 𝑠 * → J × t J Cn MetOpen ⁡ dist ⁡ ℝ 𝑠 * ⊆ J × t J Cn K
13 4 8 12 mp2an ⊢ J × t J Cn MetOpen ⁡ dist ⁡ ℝ 𝑠 * ⊆ J × t J Cn K
14 1 5 6 xmetdcn2 ⊢ D ∈ ∞Met ⁡ X → D ∈ J × t J Cn MetOpen ⁡ dist ⁡ ℝ 𝑠 *
15 13 14 sselid ⊢ D ∈ ∞Met ⁡ X → D ∈ J × t J Cn K