Theorem xpsspw

Description: A Cartesian product is included in the power of the power of the union of its arguments. (Contributed by NM, 13-Sep-2006)

	Ref	Expression
Assertion	xpsspw	|- ( A X. B ) C_ ~P ~P ( A u. B )

Proof

Step	Hyp	Ref	Expression
1		relxp	|- Rel ( A X. B )
2		opelxp	|- ( <. x , y >. e. ( A X. B ) <-> ( x e. A /\ y e. B ) )
3		snssi	|- ( x e. A -> { x } C_ A )
4		ssun3	|- ( { x } C_ A -> { x } C_ ( A u. B ) )
5	3 4	syl	|- ( x e. A -> { x } C_ ( A u. B ) )
6		vsnex	|- { x } e. _V
7	6	elpw	|- ( { x } e. ~P ( A u. B ) <-> { x } C_ ( A u. B ) )
8	5 7	sylibr	|- ( x e. A -> { x } e. ~P ( A u. B ) )
9	8	adantr	|- ( ( x e. A /\ y e. B ) -> { x } e. ~P ( A u. B ) )
10		df-pr	|- { x , y } = ( { x } u. { y } )
11		snssi	|- ( y e. B -> { y } C_ B )
12		ssun4	|- ( { y } C_ B -> { y } C_ ( A u. B ) )
13	11 12	syl	|- ( y e. B -> { y } C_ ( A u. B ) )
14	5 13	anim12i	|- ( ( x e. A /\ y e. B ) -> ( { x } C_ ( A u. B ) /\ { y } C_ ( A u. B ) ) )
15		unss	|- ( ( { x } C_ ( A u. B ) /\ { y } C_ ( A u. B ) ) <-> ( { x } u. { y } ) C_ ( A u. B ) )
16	14 15	sylib	|- ( ( x e. A /\ y e. B ) -> ( { x } u. { y } ) C_ ( A u. B ) )
17	10 16	eqsstrid	|- ( ( x e. A /\ y e. B ) -> { x , y } C_ ( A u. B ) )
18		zfpair2	|- { x , y } e. _V
19	18	elpw	|- ( { x , y } e. ~P ( A u. B ) <-> { x , y } C_ ( A u. B ) )
20	17 19	sylibr	|- ( ( x e. A /\ y e. B ) -> { x , y } e. ~P ( A u. B ) )
21	9 20	jca	|- ( ( x e. A /\ y e. B ) -> ( { x } e. ~P ( A u. B ) /\ { x , y } e. ~P ( A u. B ) ) )
22		prex	|- { { x } , { x , y } } e. _V
23	22	elpw	|- ( { { x } , { x , y } } e. ~P ~P ( A u. B ) <-> { { x } , { x , y } } C_ ~P ( A u. B ) )
24		vex	|- x e. _V
25		vex	|- y e. _V
26	24 25	dfop	|- <. x , y >. = { { x } , { x , y } }
27	26	eleq1i	|- ( <. x , y >. e. ~P ~P ( A u. B ) <-> { { x } , { x , y } } e. ~P ~P ( A u. B ) )
28	6 18	prss	|- ( ( { x } e. ~P ( A u. B ) /\ { x , y } e. ~P ( A u. B ) ) <-> { { x } , { x , y } } C_ ~P ( A u. B ) )
29	23 27 28	3bitr4ri	|- ( ( { x } e. ~P ( A u. B ) /\ { x , y } e. ~P ( A u. B ) ) <-> <. x , y >. e. ~P ~P ( A u. B ) )
30	21 29	sylib	|- ( ( x e. A /\ y e. B ) -> <. x , y >. e. ~P ~P ( A u. B ) )
31	2 30	sylbi	|- ( <. x , y >. e. ( A X. B ) -> <. x , y >. e. ~P ~P ( A u. B ) )
32	1 31	relssi	|- ( A X. B ) C_ ~P ~P ( A u. B )