Theorem tustopn

Description: The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017)

	Ref	Expression
Hypotheses	tuslem.k	|- K = ( toUnifSp ` U )
	tustopn.j	|- J = ( unifTop ` U )
Assertion	tustopn	|- ( U e. ( UnifOn ` X ) -> J = ( TopOpen ` K ) )

Proof

Step	Hyp	Ref	Expression
1		tuslem.k	|- K = ( toUnifSp ` U )
2		tustopn.j	|- J = ( unifTop ` U )
3	1	tuslem	|- ( U e. ( UnifOn ` X ) -> ( X = ( Base ` K ) /\ U = ( UnifSet ` K ) /\ ( unifTop ` U ) = ( TopOpen ` K ) ) )
4	3	simp3d	|- ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = ( TopOpen ` K ) )
5	2 4	eqtrid	|- ( U e. ( UnifOn ` X ) -> J = ( TopOpen ` K ) )