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 UnifOn (X) \to ⋃ U = X \times X$

Step	Hyp	Ref	Expression
1		ustbasel	$⊢ U \in UnifOn (X) \to X \times X \in U$
2		ustssxp	$⊢ (U \in UnifOn (X) \land u \in U) \to u \subseteq X \times X$
3	2	ralrimiva	$⊢ U \in UnifOn (X) \to \forall u \in U u \subseteq X \times X$
4		pwssb	$⊢ U \subseteq 𝒫 (X \times X) \leftrightarrow \forall u \in U u \subseteq X \times X$
5	3 4	sylibr	$⊢ U \in UnifOn (X) \to U \subseteq 𝒫 (X \times X)$
6		elpwuni	$⊢ X \times X \in U \to (U \subseteq 𝒫 (X \times X) \leftrightarrow ⋃ U = X \times X)$
7	6	biimpa	$⊢ (X \times X \in U \land U \subseteq 𝒫 (X \times X)) \to ⋃ U = X \times X$
8	1 5 7	syl2anc	$⊢ U \in UnifOn (X) \to ⋃ U = X \times X$

Metamath Proof Explorer