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