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 ‘ 𝐴 ) )