Metamath Proof Explorer


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 eqtrid ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐽 = ( TopOpen β€˜ 𝐾 ) )