Step |
Hyp |
Ref |
Expression |
1 |
|
pmvalg |
|- ( ( A e. V /\ B e. W ) -> ( A ^pm B ) = { g e. ~P ( B X. A ) | Fun g } ) |
2 |
1
|
eleq2d |
|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^pm B ) <-> C e. { g e. ~P ( B X. A ) | Fun g } ) ) |
3 |
|
funeq |
|- ( g = C -> ( Fun g <-> Fun C ) ) |
4 |
3
|
elrab |
|- ( C e. { g e. ~P ( B X. A ) | Fun g } <-> ( C e. ~P ( B X. A ) /\ Fun C ) ) |
5 |
2 4
|
bitrdi |
|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^pm B ) <-> ( C e. ~P ( B X. A ) /\ Fun C ) ) ) |
6 |
5
|
biancomd |
|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^pm B ) <-> ( Fun C /\ C e. ~P ( B X. A ) ) ) ) |
7 |
|
elex |
|- ( C e. ~P ( B X. A ) -> C e. _V ) |
8 |
7
|
a1i |
|- ( ( A e. V /\ B e. W ) -> ( C e. ~P ( B X. A ) -> C e. _V ) ) |
9 |
|
xpexg |
|- ( ( B e. W /\ A e. V ) -> ( B X. A ) e. _V ) |
10 |
9
|
ancoms |
|- ( ( A e. V /\ B e. W ) -> ( B X. A ) e. _V ) |
11 |
|
ssexg |
|- ( ( C C_ ( B X. A ) /\ ( B X. A ) e. _V ) -> C e. _V ) |
12 |
11
|
expcom |
|- ( ( B X. A ) e. _V -> ( C C_ ( B X. A ) -> C e. _V ) ) |
13 |
10 12
|
syl |
|- ( ( A e. V /\ B e. W ) -> ( C C_ ( B X. A ) -> C e. _V ) ) |
14 |
|
elpwg |
|- ( C e. _V -> ( C e. ~P ( B X. A ) <-> C C_ ( B X. A ) ) ) |
15 |
14
|
a1i |
|- ( ( A e. V /\ B e. W ) -> ( C e. _V -> ( C e. ~P ( B X. A ) <-> C C_ ( B X. A ) ) ) ) |
16 |
8 13 15
|
pm5.21ndd |
|- ( ( A e. V /\ B e. W ) -> ( C e. ~P ( B X. A ) <-> C C_ ( B X. A ) ) ) |
17 |
16
|
anbi2d |
|- ( ( A e. V /\ B e. W ) -> ( ( Fun C /\ C e. ~P ( B X. A ) ) <-> ( Fun C /\ C C_ ( B X. A ) ) ) ) |
18 |
6 17
|
bitrd |
|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^pm B ) <-> ( Fun C /\ C C_ ( B X. A ) ) ) ) |