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 𝒫 A

Proof

Step Hyp Ref Expression
1 uniexg A V A V
2 1 pwexd A V 𝒫 A V
3 pwuni A 𝒫 A
4 fiss 𝒫 A V A 𝒫 A fi A fi 𝒫 A
5 2 3 4 sylancl A V fi A fi 𝒫 A
6 ssinss1 x A x y A
7 vex x V
8 7 elpw x 𝒫 A x A
9 7 inex1 x y V
10 9 elpw x y 𝒫 A x y A
11 6 8 10 3imtr4i x 𝒫 A x y 𝒫 A
12 11 adantr x 𝒫 A y 𝒫 A x y 𝒫 A
13 12 rgen2 x 𝒫 A y 𝒫 A x y 𝒫 A
14 inficl 𝒫 A V x 𝒫 A y 𝒫 A x y 𝒫 A fi 𝒫 A = 𝒫 A
15 2 14 syl A V x 𝒫 A y 𝒫 A x y 𝒫 A fi 𝒫 A = 𝒫 A
16 13 15 mpbii A V fi 𝒫 A = 𝒫 A
17 5 16 sseqtrd A V fi A 𝒫 A
18 fvprc ¬ A V fi A =
19 0ss 𝒫 A
20 18 19 eqsstrdi ¬ A V fi A 𝒫 A
21 17 20 pm2.61i fi A 𝒫 A