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

Metamath Proof Explorer

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 )