Metamath Proof Explorer


Theorem cover2

Description: Two ways of expressing the statement "there is a cover of A by elements of B such that for each set in the cover, ph ". Note that ph and x must be distinct. (Contributed by Jeff Madsen, 20-Jun-2010)

Ref Expression
Hypotheses cover2.1 BV
cover2.2 A=B
Assertion cover2 xAyBxyφz𝒫Bz=Ayzφ

Proof

Step Hyp Ref Expression
1 cover2.1 BV
2 cover2.2 A=B
3 ssrab2 yB|φB
4 1 3 elpwi2 yB|φ𝒫B
5 nfra1 xxAyBxyφ
6 3 unissi yB|φB
7 6 sseli xyB|φxB
8 7 2 eleqtrrdi xyB|φxA
9 rsp xAyBxyφxAyBxyφ
10 elunirab xyB|φyBxyφ
11 9 10 syl6ibr xAyBxyφxAxyB|φ
12 8 11 impbid2 xAyBxyφxyB|φxA
13 5 12 alrimi xAyBxyφxxyB|φxA
14 dfcleq yB|φ=AxxyB|φxA
15 13 14 sylibr xAyBxyφyB|φ=A
16 nfrab1 _yyB|φ
17 16 nfeq2 yz=yB|φ
18 eleq2 z=yB|φyzyyB|φ
19 rabid yyB|φyBφ
20 19 simprbi yyB|φφ
21 18 20 syl6bi z=yB|φyzφ
22 17 21 ralrimi z=yB|φyzφ
23 unieq z=yB|φz=yB|φ
24 23 eqeq1d z=yB|φz=AyB|φ=A
25 24 anbi1d z=yB|φz=AyzφyB|φ=Ayzφ
26 22 25 mpbiran2d z=yB|φz=AyzφyB|φ=A
27 26 rspcev yB|φ𝒫ByB|φ=Az𝒫Bz=Ayzφ
28 4 15 27 sylancr xAyBxyφz𝒫Bz=Ayzφ
29 elpwi z𝒫BzB
30 r19.29r yzxyyzφyzxyφ
31 30 expcom yzφyzxyyzxyφ
32 ssrexv zByzxyφyBxyφ
33 31 32 sylan9r zByzφyzxyyBxyφ
34 29 33 sylan z𝒫ByzφyzxyyBxyφ
35 eleq2 z=AxzxA
36 35 biimpar z=AxAxz
37 eluni2 xzyzxy
38 36 37 sylib z=AxAyzxy
39 34 38 impel z𝒫Byzφz=AxAyBxyφ
40 39 anassrs z𝒫Byzφz=AxAyBxyφ
41 40 ralrimiva z𝒫Byzφz=AxAyBxyφ
42 41 anasss z𝒫Byzφz=AxAyBxyφ
43 42 ancom2s z𝒫Bz=AyzφxAyBxyφ
44 43 rexlimiva z𝒫Bz=AyzφxAyBxyφ
45 28 44 impbii xAyBxyφz𝒫Bz=Ayzφ