This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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