Theorem tustopn

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

	Ref	Expression
Hypotheses	tuslem.k	$$⊢K=\mathrm{toUnifSp}\left(U\right)$$
	tustopn.j	$$⊢J=\mathrm{unifTop}\left(U\right)$$
Assertion	tustopn	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to J=\mathrm{TopOpen}\left(K\right)$$

Proof

Step	Hyp	Ref	Expression
1		tuslem.k	$$⊢K=\mathrm{toUnifSp}\left(U\right)$$
2		tustopn.j	$$⊢J=\mathrm{unifTop}\left(U\right)$$
3	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)$$
4	3	simp3d	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{unifTop}\left(U\right)=\mathrm{TopOpen}\left(K\right)$$
5	2 4	syl5eq	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to J=\mathrm{TopOpen}\left(K\right)$$