Step |
Hyp |
Ref |
Expression |
1 |
|
distop |
|- ( A e. V -> ~P A e. Top ) |
2 |
|
distop |
|- ( B e. W -> ~P B e. Top ) |
3 |
|
unipw |
|- U. ~P A = A |
4 |
3
|
eqcomi |
|- A = U. ~P A |
5 |
|
unipw |
|- U. ~P B = B |
6 |
5
|
eqcomi |
|- B = U. ~P B |
7 |
4 6
|
txuni |
|- ( ( ~P A e. Top /\ ~P B e. Top ) -> ( A X. B ) = U. ( ~P A tX ~P B ) ) |
8 |
1 2 7
|
syl2an |
|- ( ( A e. V /\ B e. W ) -> ( A X. B ) = U. ( ~P A tX ~P B ) ) |
9 |
|
eqimss2 |
|- ( ( A X. B ) = U. ( ~P A tX ~P B ) -> U. ( ~P A tX ~P B ) C_ ( A X. B ) ) |
10 |
8 9
|
syl |
|- ( ( A e. V /\ B e. W ) -> U. ( ~P A tX ~P B ) C_ ( A X. B ) ) |
11 |
|
sspwuni |
|- ( ( ~P A tX ~P B ) C_ ~P ( A X. B ) <-> U. ( ~P A tX ~P B ) C_ ( A X. B ) ) |
12 |
10 11
|
sylibr |
|- ( ( A e. V /\ B e. W ) -> ( ~P A tX ~P B ) C_ ~P ( A X. B ) ) |
13 |
|
elelpwi |
|- ( ( y e. x /\ x e. ~P ( A X. B ) ) -> y e. ( A X. B ) ) |
14 |
13
|
adantl |
|- ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> y e. ( A X. B ) ) |
15 |
|
xp1st |
|- ( y e. ( A X. B ) -> ( 1st ` y ) e. A ) |
16 |
|
snelpwi |
|- ( ( 1st ` y ) e. A -> { ( 1st ` y ) } e. ~P A ) |
17 |
14 15 16
|
3syl |
|- ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> { ( 1st ` y ) } e. ~P A ) |
18 |
|
xp2nd |
|- ( y e. ( A X. B ) -> ( 2nd ` y ) e. B ) |
19 |
|
snelpwi |
|- ( ( 2nd ` y ) e. B -> { ( 2nd ` y ) } e. ~P B ) |
20 |
14 18 19
|
3syl |
|- ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> { ( 2nd ` y ) } e. ~P B ) |
21 |
|
vsnid |
|- y e. { y } |
22 |
|
1st2nd2 |
|- ( y e. ( A X. B ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. ) |
23 |
14 22
|
syl |
|- ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. ) |
24 |
23
|
sneqd |
|- ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> { y } = { <. ( 1st ` y ) , ( 2nd ` y ) >. } ) |
25 |
21 24
|
eleqtrid |
|- ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> y e. { <. ( 1st ` y ) , ( 2nd ` y ) >. } ) |
26 |
|
simprl |
|- ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> y e. x ) |
27 |
23 26
|
eqeltrrd |
|- ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. e. x ) |
28 |
27
|
snssd |
|- ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> { <. ( 1st ` y ) , ( 2nd ` y ) >. } C_ x ) |
29 |
|
xpeq1 |
|- ( z = { ( 1st ` y ) } -> ( z X. w ) = ( { ( 1st ` y ) } X. w ) ) |
30 |
29
|
eleq2d |
|- ( z = { ( 1st ` y ) } -> ( y e. ( z X. w ) <-> y e. ( { ( 1st ` y ) } X. w ) ) ) |
31 |
29
|
sseq1d |
|- ( z = { ( 1st ` y ) } -> ( ( z X. w ) C_ x <-> ( { ( 1st ` y ) } X. w ) C_ x ) ) |
32 |
30 31
|
anbi12d |
|- ( z = { ( 1st ` y ) } -> ( ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) <-> ( y e. ( { ( 1st ` y ) } X. w ) /\ ( { ( 1st ` y ) } X. w ) C_ x ) ) ) |
33 |
|
xpeq2 |
|- ( w = { ( 2nd ` y ) } -> ( { ( 1st ` y ) } X. w ) = ( { ( 1st ` y ) } X. { ( 2nd ` y ) } ) ) |
34 |
|
fvex |
|- ( 1st ` y ) e. _V |
35 |
|
fvex |
|- ( 2nd ` y ) e. _V |
36 |
34 35
|
xpsn |
|- ( { ( 1st ` y ) } X. { ( 2nd ` y ) } ) = { <. ( 1st ` y ) , ( 2nd ` y ) >. } |
37 |
33 36
|
eqtrdi |
|- ( w = { ( 2nd ` y ) } -> ( { ( 1st ` y ) } X. w ) = { <. ( 1st ` y ) , ( 2nd ` y ) >. } ) |
38 |
37
|
eleq2d |
|- ( w = { ( 2nd ` y ) } -> ( y e. ( { ( 1st ` y ) } X. w ) <-> y e. { <. ( 1st ` y ) , ( 2nd ` y ) >. } ) ) |
39 |
37
|
sseq1d |
|- ( w = { ( 2nd ` y ) } -> ( ( { ( 1st ` y ) } X. w ) C_ x <-> { <. ( 1st ` y ) , ( 2nd ` y ) >. } C_ x ) ) |
40 |
38 39
|
anbi12d |
|- ( w = { ( 2nd ` y ) } -> ( ( y e. ( { ( 1st ` y ) } X. w ) /\ ( { ( 1st ` y ) } X. w ) C_ x ) <-> ( y e. { <. ( 1st ` y ) , ( 2nd ` y ) >. } /\ { <. ( 1st ` y ) , ( 2nd ` y ) >. } C_ x ) ) ) |
41 |
32 40
|
rspc2ev |
|- ( ( { ( 1st ` y ) } e. ~P A /\ { ( 2nd ` y ) } e. ~P B /\ ( y e. { <. ( 1st ` y ) , ( 2nd ` y ) >. } /\ { <. ( 1st ` y ) , ( 2nd ` y ) >. } C_ x ) ) -> E. z e. ~P A E. w e. ~P B ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) |
42 |
17 20 25 28 41
|
syl112anc |
|- ( ( ( A e. V /\ B e. W ) /\ ( y e. x /\ x e. ~P ( A X. B ) ) ) -> E. z e. ~P A E. w e. ~P B ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) |
43 |
42
|
expr |
|- ( ( ( A e. V /\ B e. W ) /\ y e. x ) -> ( x e. ~P ( A X. B ) -> E. z e. ~P A E. w e. ~P B ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) ) |
44 |
43
|
ralrimdva |
|- ( ( A e. V /\ B e. W ) -> ( x e. ~P ( A X. B ) -> A. y e. x E. z e. ~P A E. w e. ~P B ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) ) |
45 |
|
eltx |
|- ( ( ~P A e. Top /\ ~P B e. Top ) -> ( x e. ( ~P A tX ~P B ) <-> A. y e. x E. z e. ~P A E. w e. ~P B ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) ) |
46 |
1 2 45
|
syl2an |
|- ( ( A e. V /\ B e. W ) -> ( x e. ( ~P A tX ~P B ) <-> A. y e. x E. z e. ~P A E. w e. ~P B ( y e. ( z X. w ) /\ ( z X. w ) C_ x ) ) ) |
47 |
44 46
|
sylibrd |
|- ( ( A e. V /\ B e. W ) -> ( x e. ~P ( A X. B ) -> x e. ( ~P A tX ~P B ) ) ) |
48 |
47
|
ssrdv |
|- ( ( A e. V /\ B e. W ) -> ~P ( A X. B ) C_ ( ~P A tX ~P B ) ) |
49 |
12 48
|
eqssd |
|- ( ( A e. V /\ B e. W ) -> ( ~P A tX ~P B ) = ~P ( A X. B ) ) |