Theorem tmstopn

Description: The topology of a constructed metric. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	tmsbas.k	⊢ 𝐾 = ( toMetSp ‘ 𝐷 )
	tmstopn.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion	tmstopn	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 = ( TopOpen ‘ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		tmsbas.k	⊢ 𝐾 = ( toMetSp ‘ 𝐷 )
2		tmstopn.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3		eqid	⊢ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ }
4	3 1	tmslem	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋 = ( Base ‘ 𝐾 ) ∧ 𝐷 = ( dist ‘ 𝐾 ) ∧ ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐾 ) ) )
5	4	simp3d	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐾 ) )
6	2 5	syl5eq	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 = ( TopOpen ‘ 𝐾 ) )