Theorem tusunif

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

	Ref	Expression
Hypothesis	tuslem.k	$$⊢K=\mathrm{toUnifSp}\left(U\right)$$
Assertion	tusunif	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to U=\mathrm{UnifSet}\left(K\right)$$

Proof

Step	Hyp	Ref	Expression
1		tuslem.k	$$⊢K=\mathrm{toUnifSp}\left(U\right)$$
2	1	tuslem	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \left(X={\mathrm{Base}}_K\wedge U=\mathrm{UnifSet}\left(K\right)\wedge \mathrm{unifTop}\left(U\right)=\mathrm{TopOpen}\left(K\right)\right)$$
3	2	simp2d	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to U=\mathrm{UnifSet}\left(K\right)$$