Theorem tusunif

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

	Ref	Expression
Hypothesis	tuslem.k	|- K = ( toUnifSp ` U )
Assertion	tusunif	|- ( U e. ( UnifOn ` X ) -> U = ( UnifSet ` K ) )

Proof

Step	Hyp	Ref	Expression
1		tuslem.k	|- K = ( toUnifSp ` U )
2	1	tuslem	|- ( U e. ( UnifOn ` X ) -> ( X = ( Base ` K ) /\ U = ( UnifSet ` K ) /\ ( unifTop ` U ) = ( TopOpen ` K ) ) )
3	2	simp2d	|- ( U e. ( UnifOn ` X ) -> U = ( UnifSet ` K ) )