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 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
xmetdcn.2 ⊒ 𝐾 = ( ordTop β€˜ ≀ )
Assertion xmetdcn ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐷 ∈ ( ( 𝐽 Γ—t 𝐽 ) Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 xmetdcn2.1 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
2 xmetdcn.2 ⊒ 𝐾 = ( ordTop β€˜ ≀ )
3 letopon ⊒ ( ordTop β€˜ ≀ ) ∈ ( TopOn β€˜ ℝ* )
4 2 3 eqeltri ⊒ 𝐾 ∈ ( TopOn β€˜ ℝ* )
5 eqid ⊒ ( dist β€˜ ℝ*𝑠 ) = ( dist β€˜ ℝ*𝑠 )
6 eqid ⊒ ( MetOpen β€˜ ( dist β€˜ ℝ*𝑠 ) ) = ( MetOpen β€˜ ( dist β€˜ ℝ*𝑠 ) )
7 5 6 xrsmopn ⊒ ( ordTop β€˜ ≀ ) βŠ† ( MetOpen β€˜ ( dist β€˜ ℝ*𝑠 ) )
8 2 7 eqsstri ⊒ 𝐾 βŠ† ( MetOpen β€˜ ( dist β€˜ ℝ*𝑠 ) )
9 5 xrsxmet ⊒ ( dist β€˜ ℝ*𝑠 ) ∈ ( ∞Met β€˜ ℝ* )
10 6 mopnuni ⊒ ( ( dist β€˜ ℝ*𝑠 ) ∈ ( ∞Met β€˜ ℝ* ) β†’ ℝ* = βˆͺ ( MetOpen β€˜ ( dist β€˜ ℝ*𝑠 ) ) )
11 9 10 ax-mp ⊒ ℝ* = βˆͺ ( MetOpen β€˜ ( dist β€˜ ℝ*𝑠 ) )
12 11 cnss2 ⊒ ( ( 𝐾 ∈ ( TopOn β€˜ ℝ* ) ∧ 𝐾 βŠ† ( MetOpen β€˜ ( dist β€˜ ℝ*𝑠 ) ) ) β†’ ( ( 𝐽 Γ—t 𝐽 ) Cn ( MetOpen β€˜ ( dist β€˜ ℝ*𝑠 ) ) ) βŠ† ( ( 𝐽 Γ—t 𝐽 ) Cn 𝐾 ) )
13 4 8 12 mp2an ⊒ ( ( 𝐽 Γ—t 𝐽 ) Cn ( MetOpen β€˜ ( dist β€˜ ℝ*𝑠 ) ) ) βŠ† ( ( 𝐽 Γ—t 𝐽 ) Cn 𝐾 )
14 1 5 6 xmetdcn2 ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐷 ∈ ( ( 𝐽 Γ—t 𝐽 ) Cn ( MetOpen β€˜ ( dist β€˜ ℝ*𝑠 ) ) ) )
15 13 14 sselid ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐷 ∈ ( ( 𝐽 Γ—t 𝐽 ) Cn 𝐾 ) )