Metamath Proof Explorer


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 snex
 |-  { 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 snex
 |-  { 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 )