Theorem tusbas

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

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

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	simp1d	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to X={\mathrm{Base}}_K$$