Metamath Proof Explorer

Theorem coprprop

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

Ref Expression
Hypotheses brprop.a 
|- ( ph -> A e. V )
brprop.b 
|- ( ph -> B e. W )
brprop.c 
|- ( ph -> C e. V )
brprop.d 
|- ( ph -> D e. W )
mptprop.1 
|- ( ph -> A =/= C )
coprprop.e 
|- ( ph -> E e. X )
coprprop.f 
|- ( ph -> F e. X )
coprprop.1 
|- ( ph -> E =/= F )
Assertion coprprop 
|- ( ph -> ( { <. A , B >. , <. C , D >. } o. { <. E , A >. , <. F , C >. } ) = { <. E , B >. , <. F , D >. } )

Proof

Step Hyp Ref Expression
1 brprop.a 
 |-  ( ph -> A e. V )
2 brprop.b 
 |-  ( ph -> B e. W )
3 brprop.c 
 |-  ( ph -> C e. V )
4 brprop.d 
 |-  ( ph -> D e. W )
5 mptprop.1 
 |-  ( ph -> A =/= C )
6 coprprop.e 
 |-  ( ph -> E e. X )
7 coprprop.f 
 |-  ( ph -> F e. X )
8 coprprop.1 
 |-  ( ph -> E =/= F )
9 coundir 
 |-  ( ( { <. A , B >. } u. { <. C , D >. } ) o. { <. E , A >. } ) = ( ( { <. A , B >. } o. { <. E , A >. } ) u. ( { <. C , D >. } o. { <. E , A >. } ) )
10 1 2 6 cosnop 
 |-  ( ph -> ( { <. A , B >. } o. { <. E , A >. } ) = { <. E , B >. } )
11 5 necomd 
 |-  ( ph -> C =/= A )
12 4 6 11 cosnopne 
 |-  ( ph -> ( { <. C , D >. } o. { <. E , A >. } ) = (/) )
13 10 12 uneq12d 
 |-  ( ph -> ( ( { <. A , B >. } o. { <. E , A >. } ) u. ( { <. C , D >. } o. { <. E , A >. } ) ) = ( { <. E , B >. } u. (/) ) )
14 un0 
 |-  ( { <. E , B >. } u. (/) ) = { <. E , B >. }
15 13 14 eqtrdi 
 |-  ( ph -> ( ( { <. A , B >. } o. { <. E , A >. } ) u. ( { <. C , D >. } o. { <. E , A >. } ) ) = { <. E , B >. } )
16 9 15 syl5eq 
 |-  ( ph -> ( ( { <. A , B >. } u. { <. C , D >. } ) o. { <. E , A >. } ) = { <. E , B >. } )
17 coundir 
 |-  ( ( { <. A , B >. } u. { <. C , D >. } ) o. { <. F , C >. } ) = ( ( { <. A , B >. } o. { <. F , C >. } ) u. ( { <. C , D >. } o. { <. F , C >. } ) )
18 2 7 5 cosnopne 
 |-  ( ph -> ( { <. A , B >. } o. { <. F , C >. } ) = (/) )
19 3 4 7 cosnop 
 |-  ( ph -> ( { <. C , D >. } o. { <. F , C >. } ) = { <. F , D >. } )
20 18 19 uneq12d 
 |-  ( ph -> ( ( { <. A , B >. } o. { <. F , C >. } ) u. ( { <. C , D >. } o. { <. F , C >. } ) ) = ( (/) u. { <. F , D >. } ) )
21 0un 
 |-  ( (/) u. { <. F , D >. } ) = { <. F , D >. }
22 20 21 eqtrdi 
 |-  ( ph -> ( ( { <. A , B >. } o. { <. F , C >. } ) u. ( { <. C , D >. } o. { <. F , C >. } ) ) = { <. F , D >. } )
23 17 22 syl5eq 
 |-  ( ph -> ( ( { <. A , B >. } u. { <. C , D >. } ) o. { <. F , C >. } ) = { <. F , D >. } )
24 16 23 uneq12d 
 |-  ( ph -> ( ( ( { <. A , B >. } u. { <. C , D >. } ) o. { <. E , A >. } ) u. ( ( { <. A , B >. } u. { <. C , D >. } ) o. { <. F , C >. } ) ) = ( { <. E , B >. } u. { <. F , D >. } ) )
25 df-pr 
 |-  { <. A , B >. , <. C , D >. } = ( { <. A , B >. } u. { <. C , D >. } )
26 df-pr 
 |-  { <. E , A >. , <. F , C >. } = ( { <. E , A >. } u. { <. F , C >. } )
27 25 26 coeq12i 
 |-  ( { <. A , B >. , <. C , D >. } o. { <. E , A >. , <. F , C >. } ) = ( ( { <. A , B >. } u. { <. C , D >. } ) o. ( { <. E , A >. } u. { <. F , C >. } ) )
28 coundi 
 |-  ( ( { <. A , B >. } u. { <. C , D >. } ) o. ( { <. E , A >. } u. { <. F , C >. } ) ) = ( ( ( { <. A , B >. } u. { <. C , D >. } ) o. { <. E , A >. } ) u. ( ( { <. A , B >. } u. { <. C , D >. } ) o. { <. F , C >. } ) )
29 27 28 eqtri 
 |-  ( { <. A , B >. , <. C , D >. } o. { <. E , A >. , <. F , C >. } ) = ( ( ( { <. A , B >. } u. { <. C , D >. } ) o. { <. E , A >. } ) u. ( ( { <. A , B >. } u. { <. C , D >. } ) o. { <. F , C >. } ) )
30 df-pr 
 |-  { <. E , B >. , <. F , D >. } = ( { <. E , B >. } u. { <. F , D >. } )
31 24 29 30 3eqtr4g 
 |-  ( ph -> ( { <. A , B >. , <. C , D >. } o. { <. E , A >. , <. F , C >. } ) = { <. E , B >. , <. F , D >. } )