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	|- ( A e. V -> U. A = U. ( fi ` A ) )

Proof

Step	Hyp	Ref	Expression
1		ssfii	|- ( A e. V -> A C_ ( fi ` A ) )
2	1	unissd	|- ( A e. V -> U. A C_ U. ( fi ` A ) )
3		fipwuni	|- ( fi ` A ) C_ ~P U. A
4	3	unissi	|- U. ( fi ` A ) C_ U. ~P U. A
5		unipw	|- U. ~P U. A = U. A
6	4 5	sseqtri	|- U. ( fi ` A ) C_ U. A
7	6	a1i	|- ( A e. V -> U. ( fi ` A ) C_ U. A )
8	2 7	eqssd	|- ( A e. V -> U. A = U. ( fi ` A ) )