Theorem tustps

Description: A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018)

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

Proof

Step	Hyp	Ref	Expression
1		tuslem.k	$$⊢K=\mathrm{toUnifSp}\left(U\right)$$
2		utoptopon	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{unifTop}\left(U\right)\in \mathrm{TopOn}\left(X\right)$$
3		eqid	$$⊢\mathrm{unifTop}\left(U\right)=\mathrm{unifTop}\left(U\right)$$
4	1 3	tustopn	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{unifTop}\left(U\right)=\mathrm{TopOpen}\left(K\right)$$
5	1	tusbas	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to X={\mathrm{Base}}_K$$
6	5	fveq2d	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{TopOn}\left(X\right)=\mathrm{TopOn}\left({\mathrm{Base}}_K\right)$$
7	2 4 6	3eltr3d	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{TopOpen}\left(K\right)\in \mathrm{TopOn}\left({\mathrm{Base}}_K\right)$$
8		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
9		eqid	$$⊢\mathrm{TopOpen}\left(K\right)=\mathrm{TopOpen}\left(K\right)$$
10	8 9	istps	$$⊢K\in \mathrm{TopSp}\leftrightarrow \mathrm{TopOpen}\left(K\right)\in \mathrm{TopOn}\left({\mathrm{Base}}_K\right)$$
11	7 10	sylibr	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to K\in \mathrm{TopSp}$$