Step |
Hyp |
Ref |
Expression |
1 |
|
n0 |
|- ( A =/= (/) <-> E. x x e. A ) |
2 |
|
n0 |
|- ( B =/= (/) <-> E. y y e. B ) |
3 |
1 2
|
anbi12i |
|- ( ( A =/= (/) /\ B =/= (/) ) <-> ( E. x x e. A /\ E. y y e. B ) ) |
4 |
|
exdistrv |
|- ( E. x E. y ( x e. A /\ y e. B ) <-> ( E. x x e. A /\ E. y y e. B ) ) |
5 |
3 4
|
bitr4i |
|- ( ( A =/= (/) /\ B =/= (/) ) <-> E. x E. y ( x e. A /\ y e. B ) ) |
6 |
|
opex |
|- <. x , y >. e. _V |
7 |
|
eleq1 |
|- ( z = <. x , y >. -> ( z e. ( A X. B ) <-> <. x , y >. e. ( A X. B ) ) ) |
8 |
|
opelxp |
|- ( <. x , y >. e. ( A X. B ) <-> ( x e. A /\ y e. B ) ) |
9 |
7 8
|
bitrdi |
|- ( z = <. x , y >. -> ( z e. ( A X. B ) <-> ( x e. A /\ y e. B ) ) ) |
10 |
6 9
|
spcev |
|- ( ( x e. A /\ y e. B ) -> E. z z e. ( A X. B ) ) |
11 |
|
n0 |
|- ( ( A X. B ) =/= (/) <-> E. z z e. ( A X. B ) ) |
12 |
10 11
|
sylibr |
|- ( ( x e. A /\ y e. B ) -> ( A X. B ) =/= (/) ) |
13 |
12
|
exlimivv |
|- ( E. x E. y ( x e. A /\ y e. B ) -> ( A X. B ) =/= (/) ) |
14 |
5 13
|
sylbi |
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( A X. B ) =/= (/) ) |
15 |
|
xpeq1 |
|- ( A = (/) -> ( A X. B ) = ( (/) X. B ) ) |
16 |
|
0xp |
|- ( (/) X. B ) = (/) |
17 |
15 16
|
eqtrdi |
|- ( A = (/) -> ( A X. B ) = (/) ) |
18 |
17
|
necon3i |
|- ( ( A X. B ) =/= (/) -> A =/= (/) ) |
19 |
|
xpeq2 |
|- ( B = (/) -> ( A X. B ) = ( A X. (/) ) ) |
20 |
|
xp0 |
|- ( A X. (/) ) = (/) |
21 |
19 20
|
eqtrdi |
|- ( B = (/) -> ( A X. B ) = (/) ) |
22 |
21
|
necon3i |
|- ( ( A X. B ) =/= (/) -> B =/= (/) ) |
23 |
18 22
|
jca |
|- ( ( A X. B ) =/= (/) -> ( A =/= (/) /\ B =/= (/) ) ) |
24 |
14 23
|
impbii |
|- ( ( A =/= (/) /\ B =/= (/) ) <-> ( A X. B ) =/= (/) ) |