Metamath Proof Explorer

Theorem unixp

Description: The double class union of a nonempty Cartesian product is the union of it members. (Contributed by NM, 17-Sep-2006)

Ref Expression
Assertion unixp 
|- ( ( A X. B ) =/= (/) -> U. U. ( A X. B ) = ( A u. B ) )

Proof

Step Hyp Ref Expression
1 relxp 
 |-  Rel ( A X. B )
2 relfld 
 |-  ( Rel ( A X. B ) -> U. U. ( A X. B ) = ( dom ( A X. B ) u. ran ( A X. B ) ) )
3 1 2 ax-mp 
 |-  U. U. ( A X. B ) = ( dom ( A X. B ) u. ran ( A X. B ) )
4 xpeq2 
 |-  ( B = (/) -> ( A X. B ) = ( A X. (/) ) )
5 xp0 
 |-  ( A X. (/) ) = (/)
6 4 5 eqtrdi 
 |-  ( B = (/) -> ( A X. B ) = (/) )
7 6 necon3i 
 |-  ( ( A X. B ) =/= (/) -> B =/= (/) )
8 xpeq1 
 |-  ( A = (/) -> ( A X. B ) = ( (/) X. B ) )
9 0xp 
 |-  ( (/) X. B ) = (/)
10 8 9 eqtrdi 
 |-  ( A = (/) -> ( A X. B ) = (/) )
11 10 necon3i 
 |-  ( ( A X. B ) =/= (/) -> A =/= (/) )
12 dmxp 
 |-  ( B =/= (/) -> dom ( A X. B ) = A )
13 rnxp 
 |-  ( A =/= (/) -> ran ( A X. B ) = B )
14 uneq12 
 |-  ( ( dom ( A X. B ) = A /\ ran ( A X. B ) = B ) -> ( dom ( A X. B ) u. ran ( A X. B ) ) = ( A u. B ) )
15 12 13 14 syl2an 
 |-  ( ( B =/= (/) /\ A =/= (/) ) -> ( dom ( A X. B ) u. ran ( A X. B ) ) = ( A u. B ) )
16 7 11 15 syl2anc 
 |-  ( ( A X. B ) =/= (/) -> ( dom ( A X. B ) u. ran ( A X. B ) ) = ( A u. B ) )
17 3 16 syl5eq 
 |-  ( ( A X. B ) =/= (/) -> U. U. ( A X. B ) = ( A u. B ) )