Theorem fipwss

Description: If a set is a family of subsets of some base set, then so is its finite intersection. (Contributed by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	fipwss	|- ( A C_ ~P X -> ( fi ` A ) C_ ~P X )

Proof

Step	Hyp	Ref	Expression
1		fiuni	|- ( A e. _V -> U. A = U. ( fi ` A ) )
2	1	sseq1d	|- ( A e. _V -> ( U. A C_ X <-> U. ( fi ` A ) C_ X ) )
3		sspwuni	|- ( A C_ ~P X <-> U. A C_ X )
4		sspwuni	|- ( ( fi ` A ) C_ ~P X <-> U. ( fi ` A ) C_ X )
5	2 3 4	3bitr4g	|- ( A e. _V -> ( A C_ ~P X <-> ( fi ` A ) C_ ~P X ) )
6	5	biimpa	|- ( ( A e. _V /\ A C_ ~P X ) -> ( fi ` A ) C_ ~P X )
7		fvprc	|- ( -. A e. _V -> ( fi ` A ) = (/) )
8		0ss	|- (/) C_ ~P X
9	7 8	eqsstrdi	|- ( -. A e. _V -> ( fi ` A ) C_ ~P X )
10	9	adantr	|- ( ( -. A e. _V /\ A C_ ~P X ) -> ( fi ` A ) C_ ~P X )
11	6 10	pm2.61ian	|- ( A C_ ~P X -> ( fi ` A ) C_ ~P X )