Step |
Hyp |
Ref |
Expression |
1 |
|
ssrab2 |
|- { f e. ~P ( B X. A ) | Fun f } C_ ~P ( B X. A ) |
2 |
|
xpexg |
|- ( ( B e. D /\ A e. C ) -> ( B X. A ) e. _V ) |
3 |
2
|
ancoms |
|- ( ( A e. C /\ B e. D ) -> ( B X. A ) e. _V ) |
4 |
3
|
pwexd |
|- ( ( A e. C /\ B e. D ) -> ~P ( B X. A ) e. _V ) |
5 |
|
ssexg |
|- ( ( { f e. ~P ( B X. A ) | Fun f } C_ ~P ( B X. A ) /\ ~P ( B X. A ) e. _V ) -> { f e. ~P ( B X. A ) | Fun f } e. _V ) |
6 |
1 4 5
|
sylancr |
|- ( ( A e. C /\ B e. D ) -> { f e. ~P ( B X. A ) | Fun f } e. _V ) |
7 |
|
elex |
|- ( A e. C -> A e. _V ) |
8 |
|
elex |
|- ( B e. D -> B e. _V ) |
9 |
|
xpeq2 |
|- ( x = A -> ( y X. x ) = ( y X. A ) ) |
10 |
9
|
pweqd |
|- ( x = A -> ~P ( y X. x ) = ~P ( y X. A ) ) |
11 |
10
|
rabeqdv |
|- ( x = A -> { f e. ~P ( y X. x ) | Fun f } = { f e. ~P ( y X. A ) | Fun f } ) |
12 |
|
xpeq1 |
|- ( y = B -> ( y X. A ) = ( B X. A ) ) |
13 |
12
|
pweqd |
|- ( y = B -> ~P ( y X. A ) = ~P ( B X. A ) ) |
14 |
13
|
rabeqdv |
|- ( y = B -> { f e. ~P ( y X. A ) | Fun f } = { f e. ~P ( B X. A ) | Fun f } ) |
15 |
|
df-pm |
|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } ) |
16 |
11 14 15
|
ovmpog |
|- ( ( A e. _V /\ B e. _V /\ { f e. ~P ( B X. A ) | Fun f } e. _V ) -> ( A ^pm B ) = { f e. ~P ( B X. A ) | Fun f } ) |
17 |
16
|
3expia |
|- ( ( A e. _V /\ B e. _V ) -> ( { f e. ~P ( B X. A ) | Fun f } e. _V -> ( A ^pm B ) = { f e. ~P ( B X. A ) | Fun f } ) ) |
18 |
7 8 17
|
syl2an |
|- ( ( A e. C /\ B e. D ) -> ( { f e. ~P ( B X. A ) | Fun f } e. _V -> ( A ^pm B ) = { f e. ~P ( B X. A ) | Fun f } ) ) |
19 |
6 18
|
mpd |
|- ( ( A e. C /\ B e. D ) -> ( A ^pm B ) = { f e. ~P ( B X. A ) | Fun f } ) |