Theorem tususs

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

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

Proof

Step	Hyp	Ref	Expression
1		tuslem.k	$$⊢K=\mathrm{toUnifSp}\left(U\right)$$
2	1	tusunif	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to U=\mathrm{UnifSet}\left(K\right)$$
3		ustuni	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \bigcup U=X\times X$$
4	2	unieqd	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \bigcup U=\bigcup \mathrm{UnifSet}\left(K\right)$$
5	1	tusbas	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to X={\mathrm{Base}}_K$$
6	5	sqxpeqd	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to X\times X={\mathrm{Base}}_K\times {\mathrm{Base}}_K$$
7	3 4 6	3eqtr3rd	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to {\mathrm{Base}}_K\times {\mathrm{Base}}_K=\bigcup \mathrm{UnifSet}\left(K\right)$$
8		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
9		eqid	$$⊢\mathrm{UnifSet}\left(K\right)=\mathrm{UnifSet}\left(K\right)$$
10	8 9	ussid	$$⊢{\mathrm{Base}}_K\times {\mathrm{Base}}_K=\bigcup \mathrm{UnifSet}\left(K\right)\to \mathrm{UnifSet}\left(K\right)=\mathrm{UnifSt}\left(K\right)$$
11	7 10	syl	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{UnifSet}\left(K\right)=\mathrm{UnifSt}\left(K\right)$$
12	2 11	eqtrd	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to U=\mathrm{UnifSt}\left(K\right)$$