Theorem fipwuni

Description: The set of finite intersections of a set is contained in the powerset of the union of the elements of A . (Contributed by Mario Carneiro, 24-Nov-2013) (Proof shortened by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	fipwuni	|- ( fi ` A ) C_ ~P U. A

Proof

Step	Hyp	Ref	Expression
1		uniexg	|- ( A e. _V -> U. A e. _V )
2	1	pwexd	|- ( A e. _V -> ~P U. A e. _V )
3		pwuni	|- A C_ ~P U. A
4		fiss	|- ( ( ~P U. A e. _V /\ A C_ ~P U. A ) -> ( fi ` A ) C_ ( fi ` ~P U. A ) )
5	2 3 4	sylancl	|- ( A e. _V -> ( fi ` A ) C_ ( fi ` ~P U. A ) )
6		ssinss1	|- ( x C_ U. A -> ( x i^i y ) C_ U. A )
7		vex	|- x e. _V
8	7	elpw	|- ( x e. ~P U. A <-> x C_ U. A )
9	7	inex1	|- ( x i^i y ) e. _V
10	9	elpw	|- ( ( x i^i y ) e. ~P U. A <-> ( x i^i y ) C_ U. A )
11	6 8 10	3imtr4i	|- ( x e. ~P U. A -> ( x i^i y ) e. ~P U. A )
12	11	adantr	|- ( ( x e. ~P U. A /\ y e. ~P U. A ) -> ( x i^i y ) e. ~P U. A )
13	12	rgen2	|- A. x e. ~P U. A A. y e. ~P U. A ( x i^i y ) e. ~P U. A
14		inficl	|- ( ~P U. A e. _V -> ( A. x e. ~P U. A A. y e. ~P U. A ( x i^i y ) e. ~P U. A <-> ( fi ` ~P U. A ) = ~P U. A ) )
15	2 14	syl	|- ( A e. _V -> ( A. x e. ~P U. A A. y e. ~P U. A ( x i^i y ) e. ~P U. A <-> ( fi ` ~P U. A ) = ~P U. A ) )
16	13 15	mpbii	|- ( A e. _V -> ( fi ` ~P U. A ) = ~P U. A )
17	5 16	sseqtrd	|- ( A e. _V -> ( fi ` A ) C_ ~P U. A )
18		fvprc	|- ( -. A e. _V -> ( fi ` A ) = (/) )
19		0ss	|- (/) C_ ~P U. A
20	18 19	eqsstrdi	|- ( -. A e. _V -> ( fi ` A ) C_ ~P U. A )
21	17 20	pm2.61i	|- ( fi ` A ) C_ ~P U. A