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

Metamath Proof Explorer

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