Theorem ustuni

Description: The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017)

	Ref	Expression
Assertion	ustuni	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \bigcup U=X\times X$$

Proof

Step	Hyp	Ref	Expression
1		ustbasel	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to X\times X\in U$$
2		ustssxp	$$⊢\left(U\in \mathrm{UnifOn}\left(X\right)\wedge u\in U\right)\to u\subseteq X\times X$$
3	2	ralrimiva	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \forall u\in Uu\subseteq X\times X$$
4		pwssb	$$⊢U\subseteq 𝒫\left(X\times X\right)\leftrightarrow \forall u\in Uu\subseteq X\times X$$
5	3 4	sylibr	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to U\subseteq 𝒫\left(X\times X\right)$$
6		elpwuni	$$⊢X\times X\in U\to \left(U\subseteq 𝒫\left(X\times X\right)\leftrightarrow \bigcup U=X\times X\right)$$
7	6	biimpa	$$⊢\left(X\times X\in U\wedge U\subseteq 𝒫\left(X\times X\right)\right)\to \bigcup U=X\times X$$
8	1 5 7	syl2anc	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \bigcup U=X\times X$$