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	$$⊢\phi \to A\in V$$
	brprop.b	$$⊢\phi \to B\in W$$
	brprop.c	$$⊢\phi \to C\in V$$
	brprop.d	$$⊢\phi \to D\in W$$
	mptprop.1	$$⊢\phi \to A\ne C$$
	coprprop.e	$$⊢\phi \to E\in X$$
	coprprop.f	$$⊢\phi \to F\in X$$
	coprprop.1	$$⊢\phi \to E\ne F$$
Assertion	coprprop	$$⊢\phi \to \left\{⟨A,B⟩,⟨C,D⟩\right\}\circ \left\{⟨E,A⟩,⟨F,C⟩\right\}=\left\{⟨E,B⟩,⟨F,D⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		brprop.a	$$⊢\phi \to A\in V$$
2		brprop.b	$$⊢\phi \to B\in W$$
3		brprop.c	$$⊢\phi \to C\in V$$
4		brprop.d	$$⊢\phi \to D\in W$$
5		mptprop.1	$$⊢\phi \to A\ne C$$
6		coprprop.e	$$⊢\phi \to E\in X$$
7		coprprop.f	$$⊢\phi \to F\in X$$
8		coprprop.1	$$⊢\phi \to E\ne F$$
9		coundir	$$⊢\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)\circ \left\{⟨E,A⟩\right\}=\left(\left\{⟨A,B⟩\right\}\circ \left\{⟨E,A⟩\right\}\right)\cup \left(\left\{⟨C,D⟩\right\}\circ \left\{⟨E,A⟩\right\}\right)$$
10	1 2 6	cosnop	$$⊢\phi \to \left\{⟨A,B⟩\right\}\circ \left\{⟨E,A⟩\right\}=\left\{⟨E,B⟩\right\}$$
11	5	necomd	$$⊢\phi \to C\ne A$$
12	4 6 11	cosnopne	$$⊢\phi \to \left\{⟨C,D⟩\right\}\circ \left\{⟨E,A⟩\right\}=\varnothing$$
13	10 12	uneq12d	$$⊢\phi \to \left(\left\{⟨A,B⟩\right\}\circ \left\{⟨E,A⟩\right\}\right)\cup \left(\left\{⟨C,D⟩\right\}\circ \left\{⟨E,A⟩\right\}\right)=\left\{⟨E,B⟩\right\}\cup \varnothing$$
14		un0	$$⊢\left\{⟨E,B⟩\right\}\cup \varnothing =\left\{⟨E,B⟩\right\}$$
15	13 14	eqtrdi	$$⊢\phi \to \left(\left\{⟨A,B⟩\right\}\circ \left\{⟨E,A⟩\right\}\right)\cup \left(\left\{⟨C,D⟩\right\}\circ \left\{⟨E,A⟩\right\}\right)=\left\{⟨E,B⟩\right\}$$
16	9 15	syl5eq	$$⊢\phi \to \left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)\circ \left\{⟨E,A⟩\right\}=\left\{⟨E,B⟩\right\}$$
17		coundir	$$⊢\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)\circ \left\{⟨F,C⟩\right\}=\left(\left\{⟨A,B⟩\right\}\circ \left\{⟨F,C⟩\right\}\right)\cup \left(\left\{⟨C,D⟩\right\}\circ \left\{⟨F,C⟩\right\}\right)$$
18	2 7 5	cosnopne	$$⊢\phi \to \left\{⟨A,B⟩\right\}\circ \left\{⟨F,C⟩\right\}=\varnothing$$
19	3 4 7	cosnop	$$⊢\phi \to \left\{⟨C,D⟩\right\}\circ \left\{⟨F,C⟩\right\}=\left\{⟨F,D⟩\right\}$$
20	18 19	uneq12d	$$⊢\phi \to \left(\left\{⟨A,B⟩\right\}\circ \left\{⟨F,C⟩\right\}\right)\cup \left(\left\{⟨C,D⟩\right\}\circ \left\{⟨F,C⟩\right\}\right)=\varnothing \cup \left\{⟨F,D⟩\right\}$$
21		0un	$$⊢\varnothing \cup \left\{⟨F,D⟩\right\}=\left\{⟨F,D⟩\right\}$$
22	20 21	eqtrdi	$$⊢\phi \to \left(\left\{⟨A,B⟩\right\}\circ \left\{⟨F,C⟩\right\}\right)\cup \left(\left\{⟨C,D⟩\right\}\circ \left\{⟨F,C⟩\right\}\right)=\left\{⟨F,D⟩\right\}$$
23	17 22	syl5eq	$$⊢\phi \to \left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)\circ \left\{⟨F,C⟩\right\}=\left\{⟨F,D⟩\right\}$$
24	16 23	uneq12d	$$⊢\phi \to \left(\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)\circ \left\{⟨E,A⟩\right\}\right)\cup \left(\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)\circ \left\{⟨F,C⟩\right\}\right)=\left\{⟨E,B⟩\right\}\cup \left\{⟨F,D⟩\right\}$$
25		df-pr	$$⊢\left\{⟨A,B⟩,⟨C,D⟩\right\}=\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}$$
26		df-pr	$$⊢\left\{⟨E,A⟩,⟨F,C⟩\right\}=\left\{⟨E,A⟩\right\}\cup \left\{⟨F,C⟩\right\}$$
27	25 26	coeq12i	$$⊢\left\{⟨A,B⟩,⟨C,D⟩\right\}\circ \left\{⟨E,A⟩,⟨F,C⟩\right\}=\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)\circ \left(\left\{⟨E,A⟩\right\}\cup \left\{⟨F,C⟩\right\}\right)$$
28		coundi	$$⊢\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)\circ \left(\left\{⟨E,A⟩\right\}\cup \left\{⟨F,C⟩\right\}\right)=\left(\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)\circ \left\{⟨E,A⟩\right\}\right)\cup \left(\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)\circ \left\{⟨F,C⟩\right\}\right)$$
29	27 28	eqtri	$$⊢\left\{⟨A,B⟩,⟨C,D⟩\right\}\circ \left\{⟨E,A⟩,⟨F,C⟩\right\}=\left(\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)\circ \left\{⟨E,A⟩\right\}\right)\cup \left(\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)\circ \left\{⟨F,C⟩\right\}\right)$$
30		df-pr	$$⊢\left\{⟨E,B⟩,⟨F,D⟩\right\}=\left\{⟨E,B⟩\right\}\cup \left\{⟨F,D⟩\right\}$$
31	24 29 30	3eqtr4g	$$⊢\phi \to \left\{⟨A,B⟩,⟨C,D⟩\right\}\circ \left\{⟨E,A⟩,⟨F,C⟩\right\}=\left\{⟨E,B⟩,⟨F,D⟩\right\}$$