Metamath Proof Explorer

Theorem unixpss

Description: The double class union of a Cartesian product is included in the union of its arguments. (Contributed by NM, 16-Sep-2006)

Ref Expression
Assertion unixpss 
|- U. U. ( A X. B ) C_ ( A u. B )

Proof

Step Hyp Ref Expression
1 xpsspw 
 |-  ( A X. B ) C_ ~P ~P ( A u. B )
2 1 unissi 
 |-  U. ( A X. B ) C_ U. ~P ~P ( A u. B )
3 unipw 
 |-  U. ~P ~P ( A u. B ) = ~P ( A u. B )
4 2 3 sseqtri 
 |-  U. ( A X. B ) C_ ~P ( A u. B )
5 4 unissi 
 |-  U. U. ( A X. B ) C_ U. ~P ( A u. B )
6 unipw 
 |-  U. ~P ( A u. B ) = ( A u. B )
7 5 6 sseqtri 
 |-  U. U. ( A X. B ) C_ ( A u. B )