Metamath Proof Explorer


Theorem cosnop

Description: Composition of two ordered pair singletons with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023)

Ref Expression
Hypotheses cosnop.a
|- ( ph -> A e. V )
cosnop.b
|- ( ph -> B e. W )
cosnop.c
|- ( ph -> C e. X )
Assertion cosnop
|- ( ph -> ( { <. A , B >. } o. { <. C , A >. } ) = { <. C , B >. } )

Proof

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