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

Metamath Proof Explorer

Theorem fiuni

Description: The union of the finite intersections of a set is simply the union of the set itself. (Contributed by Jeff Hankins, 5-Sep-2009) (Revised by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion fiuni ( 𝐴 ∈ 𝑉 → ∪ 𝐴 = ∪ ( fi ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ssfii ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( fi ‘ 𝐴 ) )
2 1 unissd ⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 ⊆ ∪ ( fi ‘ 𝐴 ) )
3 fipwuni ⊢ ( fi ‘ 𝐴 ) ⊆ 𝒫 ∪ 𝐴
4 3 unissi ⊢ ∪ ( fi ‘ 𝐴 ) ⊆ ∪ 𝒫 ∪ 𝐴
5 unipw ⊢ ∪ 𝒫 ∪ 𝐴 = ∪ 𝐴
6 4 5 sseqtri ⊢ ∪ ( fi ‘ 𝐴 ) ⊆ ∪ 𝐴
7 6 a1i ⊢ ( 𝐴 ∈ 𝑉 → ∪ ( fi ‘ 𝐴 ) ⊆ ∪ 𝐴 )
8 2 7 eqssd ⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 = ∪ ( fi ‘ 𝐴 ) )