Theorem xmetutop

Description: The topology induced by a uniform structure generated by an extended metric D is that metric's open sets. (Contributed by Thierry Arnoux, 11-Mar-2018)

	Ref	Expression
Assertion	xmetutop	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		xmetpsmet	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
2		psmetutop	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
3	1 2	sylan2	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
4		eqid	⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
5	4	mopnval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
6	5	adantl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
7	3 6	eqtr4d	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) )