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

Metamath Proof Explorer

Theorem msdcn

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, 5-Oct-2015)

Ref Expression
Hypotheses msdcn.x ⊢ 𝑋 = ( Base ‘ 𝑀 )
msdcn.d ⊢ 𝐷 = ( dist ‘ 𝑀 )
msdcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑀 )
msdcn.2 ⊢ 𝐾 = ( topGen ‘ ran (,) )
Assertion msdcn ( 𝑀 ∈ MetSp → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 msdcn.x ⊢ 𝑋 = ( Base ‘ 𝑀 )
2 msdcn.d ⊢ 𝐷 = ( dist ‘ 𝑀 )
3 msdcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑀 )
4 msdcn.2 ⊢ 𝐾 = ( topGen ‘ ran (,) )
5 1 2 msmet2 ⊢ ( 𝑀 ∈ MetSp → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) )
6 eqid ⊢ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) )
7 6 4 metdcn2 ⊢ ( ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ×t ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ) Cn 𝐾 ) )
8 5 7 syl ⊢ ( 𝑀 ∈ MetSp → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ×t ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ) Cn 𝐾 ) )
9 2 reseq1i ⊢ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) )
10 3 1 9 mstopn ⊢ ( 𝑀 ∈ MetSp → 𝐽 = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) )
11 10 10 oveq12d ⊢ ( 𝑀 ∈ MetSp → ( 𝐽 ×t 𝐽 ) = ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ×t ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ) )
12 11 oveq1d ⊢ ( 𝑀 ∈ MetSp → ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) = ( ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ×t ( MetOpen ‘ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ) Cn 𝐾 ) )
13 8 12 eleqtrrd ⊢ ( 𝑀 ∈ MetSp → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )