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	$$⊢\phi \to A\in V$$
	cosnop.b	$$⊢\phi \to B\in W$$
	cosnop.c	$$⊢\phi \to C\in X$$
Assertion	cosnop	$$⊢\phi \to \left\{⟨A,B⟩\right\}\circ \left\{⟨C,A⟩\right\}=\left\{⟨C,B⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cosnop.a	$$⊢\phi \to A\in V$$
2		cosnop.b	$$⊢\phi \to B\in W$$
3		cosnop.c	$$⊢\phi \to C\in X$$
4		snnzg	$$⊢A\in V\to \left\{A\right\}\ne \varnothing$$
5		xpco	$$⊢\left\{A\right\}\ne \varnothing \to \left(\left\{A\right\}\times \left\{B\right\}\right)\circ \left(\left\{C\right\}\times \left\{A\right\}\right)=\left\{C\right\}\times \left\{B\right\}$$
6	1 4 5	3syl	$$⊢\phi \to \left(\left\{A\right\}\times \left\{B\right\}\right)\circ \left(\left\{C\right\}\times \left\{A\right\}\right)=\left\{C\right\}\times \left\{B\right\}$$
7		xpsng	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{A\right\}\times \left\{B\right\}=\left\{⟨A,B⟩\right\}$$
8	1 2 7	syl2anc	$$⊢\phi \to \left\{A\right\}\times \left\{B\right\}=\left\{⟨A,B⟩\right\}$$
9		xpsng	$$⊢\left(C\in X\wedge A\in V\right)\to \left\{C\right\}\times \left\{A\right\}=\left\{⟨C,A⟩\right\}$$
10	3 1 9	syl2anc	$$⊢\phi \to \left\{C\right\}\times \left\{A\right\}=\left\{⟨C,A⟩\right\}$$
11	8 10	coeq12d	$$⊢\phi \to \left(\left\{A\right\}\times \left\{B\right\}\right)\circ \left(\left\{C\right\}\times \left\{A\right\}\right)=\left\{⟨A,B⟩\right\}\circ \left\{⟨C,A⟩\right\}$$
12		xpsng	$$⊢\left(C\in X\wedge B\in W\right)\to \left\{C\right\}\times \left\{B\right\}=\left\{⟨C,B⟩\right\}$$
13	3 2 12	syl2anc	$$⊢\phi \to \left\{C\right\}\times \left\{B\right\}=\left\{⟨C,B⟩\right\}$$
14	6 11 13	3eqtr3d	$$⊢\phi \to \left\{⟨A,B⟩\right\}\circ \left\{⟨C,A⟩\right\}=\left\{⟨C,B⟩\right\}$$