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