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 φ A V
brprop.b φ B W
brprop.c φ C V
brprop.d φ D W
mptprop.1 φ A C
coprprop.e φ E X
coprprop.f φ F X
coprprop.1 φ E F
Assertion coprprop φ A B C D E A F C = E B F D

Proof

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