Metamath Proof Explorer

Theorem unixp0

Description: A Cartesian product is empty iff its union is empty. (Contributed by NM, 20-Sep-2006)

Ref Expression
Assertion unixp0 
|- ( ( A X. B ) = (/) <-> U. ( A X. B ) = (/) )

Proof

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 ) = (/) )