Step |
Hyp |
Ref |
Expression |
1 |
|
unieq |
|- ( ( A X. B ) = (/) -> U. ( A X. B ) = U. (/) ) |
2 |
|
uni0 |
|- U. (/) = (/) |
3 |
1 2
|
eqtrdi |
|- ( ( A X. B ) = (/) -> U. ( A X. B ) = (/) ) |
4 |
|
n0 |
|- ( ( A X. B ) =/= (/) <-> E. z z e. ( A X. B ) ) |
5 |
|
elxp3 |
|- ( z e. ( A X. B ) <-> E. x E. y ( <. x , y >. = z /\ <. x , y >. e. ( A X. B ) ) ) |
6 |
|
elssuni |
|- ( <. x , y >. e. ( A X. B ) -> <. x , y >. C_ U. ( A X. B ) ) |
7 |
|
vex |
|- x e. _V |
8 |
|
vex |
|- y e. _V |
9 |
7 8
|
opnzi |
|- <. x , y >. =/= (/) |
10 |
|
ssn0 |
|- ( ( <. x , y >. C_ U. ( A X. B ) /\ <. x , y >. =/= (/) ) -> U. ( A X. B ) =/= (/) ) |
11 |
6 9 10
|
sylancl |
|- ( <. x , y >. e. ( A X. B ) -> U. ( A X. B ) =/= (/) ) |
12 |
11
|
adantl |
|- ( ( <. x , y >. = z /\ <. x , y >. e. ( A X. B ) ) -> U. ( A X. B ) =/= (/) ) |
13 |
12
|
exlimivv |
|- ( E. x E. y ( <. x , y >. = z /\ <. x , y >. e. ( A X. B ) ) -> U. ( A X. B ) =/= (/) ) |
14 |
5 13
|
sylbi |
|- ( z e. ( A X. B ) -> U. ( A X. B ) =/= (/) ) |
15 |
14
|
exlimiv |
|- ( E. z z e. ( A X. B ) -> U. ( A X. B ) =/= (/) ) |
16 |
4 15
|
sylbi |
|- ( ( A X. B ) =/= (/) -> U. ( A X. B ) =/= (/) ) |
17 |
16
|
necon4i |
|- ( U. ( A X. B ) = (/) -> ( A X. B ) = (/) ) |
18 |
3 17
|
impbii |
|- ( ( A X. B ) = (/) <-> U. ( A X. B ) = (/) ) |