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