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	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ 𝑈 = ( 𝑋 × 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ustbasel	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) ∈ 𝑈 )
2		ustssxp	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ⊆ ( 𝑋 × 𝑋 ) )
3	2	ralrimiva	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∀ 𝑢 ∈ 𝑈 𝑢 ⊆ ( 𝑋 × 𝑋 ) )
4		pwssb	⊢ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ↔ ∀ 𝑢 ∈ 𝑈 𝑢 ⊆ ( 𝑋 × 𝑋 ) )
5	3 4	sylibr	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
6		elpwuni	⊢ ( ( 𝑋 × 𝑋 ) ∈ 𝑈 → ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ↔ ∪ 𝑈 = ( 𝑋 × 𝑋 ) ) )
7	6	biimpa	⊢ ( ( ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ) → ∪ 𝑈 = ( 𝑋 × 𝑋 ) )
8	1 5 7	syl2anc	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ 𝑈 = ( 𝑋 × 𝑋 ) )