Step |
Hyp |
Ref |
Expression |
1 |
|
cosnop.a |
|- ( ph -> A e. V ) |
2 |
|
cosnop.b |
|- ( ph -> B e. W ) |
3 |
|
cosnop.c |
|- ( ph -> C e. X ) |
4 |
|
snnzg |
|- ( A e. V -> { A } =/= (/) ) |
5 |
|
xpco |
|- ( { A } =/= (/) -> ( ( { A } X. { B } ) o. ( { C } X. { A } ) ) = ( { C } X. { B } ) ) |
6 |
1 4 5
|
3syl |
|- ( ph -> ( ( { A } X. { B } ) o. ( { C } X. { A } ) ) = ( { C } X. { B } ) ) |
7 |
|
xpsng |
|- ( ( A e. V /\ B e. W ) -> ( { A } X. { B } ) = { <. A , B >. } ) |
8 |
1 2 7
|
syl2anc |
|- ( ph -> ( { A } X. { B } ) = { <. A , B >. } ) |
9 |
|
xpsng |
|- ( ( C e. X /\ A e. V ) -> ( { C } X. { A } ) = { <. C , A >. } ) |
10 |
3 1 9
|
syl2anc |
|- ( ph -> ( { C } X. { A } ) = { <. C , A >. } ) |
11 |
8 10
|
coeq12d |
|- ( ph -> ( ( { A } X. { B } ) o. ( { C } X. { A } ) ) = ( { <. A , B >. } o. { <. C , A >. } ) ) |
12 |
|
xpsng |
|- ( ( C e. X /\ B e. W ) -> ( { C } X. { B } ) = { <. C , B >. } ) |
13 |
3 2 12
|
syl2anc |
|- ( ph -> ( { C } X. { B } ) = { <. C , B >. } ) |
14 |
6 11 13
|
3eqtr3d |
|- ( ph -> ( { <. A , B >. } o. { <. C , A >. } ) = { <. C , B >. } ) |