Theorem altxpsspw

Description: An inclusion rule for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012)

	Ref	Expression
Assertion	altxpsspw	|- ( A XX. B ) C_ ~P ~P ( A u. ~P B )

Proof

Step	Hyp	Ref	Expression
1		elaltxp	|- ( z e. ( A XX. B ) <-> E. x e. A E. y e. B z = << x , y >> )
2		df-altop	|- << x , y >> = { { x } , { x , { y } } }
3		snssi	|- ( x e. A -> { x } C_ A )
4		ssun3	|- ( { x } C_ A -> { x } C_ ( A u. ~P B ) )
5	3 4	syl	|- ( x e. A -> { x } C_ ( A u. ~P B ) )
6	5	adantr	|- ( ( x e. A /\ y e. B ) -> { x } C_ ( A u. ~P B ) )
7		elun1	|- ( x e. A -> x e. ( A u. ~P B ) )
8		snssi	|- ( y e. B -> { y } C_ B )
9		vsnex	|- { y } e. _V
10	9	elpw	|- ( { y } e. ~P B <-> { y } C_ B )
11		elun2	|- ( { y } e. ~P B -> { y } e. ( A u. ~P B ) )
12	10 11	sylbir	|- ( { y } C_ B -> { y } e. ( A u. ~P B ) )
13	8 12	syl	|- ( y e. B -> { y } e. ( A u. ~P B ) )
14	7 13	anim12i	|- ( ( x e. A /\ y e. B ) -> ( x e. ( A u. ~P B ) /\ { y } e. ( A u. ~P B ) ) )
15		vex	|- x e. _V
16	15 9	prss	|- ( ( x e. ( A u. ~P B ) /\ { y } e. ( A u. ~P B ) ) <-> { x , { y } } C_ ( A u. ~P B ) )
17	14 16	sylib	|- ( ( x e. A /\ y e. B ) -> { x , { y } } C_ ( A u. ~P B ) )
18		prex	|- { { x } , { x , { y } } } e. _V
19	18	elpw	|- ( { { x } , { x , { y } } } e. ~P ~P ( A u. ~P B ) <-> { { x } , { x , { y } } } C_ ~P ( A u. ~P B ) )
20		vsnex	|- { x } e. _V
21		prex	|- { x , { y } } e. _V
22	20 21	prsspw	|- ( { { x } , { x , { y } } } C_ ~P ( A u. ~P B ) <-> ( { x } C_ ( A u. ~P B ) /\ { x , { y } } C_ ( A u. ~P B ) ) )
23	19 22	bitri	|- ( { { x } , { x , { y } } } e. ~P ~P ( A u. ~P B ) <-> ( { x } C_ ( A u. ~P B ) /\ { x , { y } } C_ ( A u. ~P B ) ) )
24	6 17 23	sylanbrc	|- ( ( x e. A /\ y e. B ) -> { { x } , { x , { y } } } e. ~P ~P ( A u. ~P B ) )
25	2 24	eqeltrid	|- ( ( x e. A /\ y e. B ) -> << x , y >> e. ~P ~P ( A u. ~P B ) )
26		eleq1a	|- ( << x , y >> e. ~P ~P ( A u. ~P B ) -> ( z = << x , y >> -> z e. ~P ~P ( A u. ~P B ) ) )
27	25 26	syl	|- ( ( x e. A /\ y e. B ) -> ( z = << x , y >> -> z e. ~P ~P ( A u. ~P B ) ) )
28	27	rexlimivv	|- ( E. x e. A E. y e. B z = << x , y >> -> z e. ~P ~P ( A u. ~P B ) )
29	1 28	sylbi	|- ( z e. ( A XX. B ) -> z e. ~P ~P ( A u. ~P B ) )
30	29	ssriv	|- ( A XX. B ) C_ ~P ~P ( A u. ~P B )