This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )