Elegant solution of a problem about binary relations Let $f$, $g$, $a$, $b$ are binary relations on some set.
I want an elegant proof that $(a\circ f^{-1})\cap(g^{-1}\circ b) \ne \varnothing \Leftrightarrow (\operatorname{dom}a\times\operatorname{dom}b)\cap f\ne\varnothing \wedge (\operatorname{im}a\times\operatorname{im}b)\cap g\ne\varnothing$.
I have a solution myself (I have reduced it to the special case when $\operatorname{card}a=\operatorname{card}b=1$.) But I want a more direct and more elegant proof.
 A: This is too long for a comment. I will denote your binary relations on a certain set $S$ by capital letters: $F,G,A,B$. If $(x,y)\in(A\circ F^{-1})\cap(G^{-1}\cap B)$ then for some $z,w\in S$ we have the relations
$$xF^{-1}z,\ zAy,\ xBw,\ wG^{-1}y\,$$
which is equivalent to
$$zFx,\ zAy,\ xBw,\ yGw\,.$$
We want to prove that $\bigl(\mathrm{Dom}(A)\times\mathrm{Im}(B)\bigr)\cap F\ne\emptyset$. The unique available pair in $F$ from the hypothesis above is $(z,x)$, and $z\in\mathrm{Dom}(A)$, but it is unknown if $x\in\mathrm{Im}(B)$. The only thing we know is that $x\in\mathrm{Dom}(B)$. In other words, we are able to prove only that $\bigl(\mathrm{Dom}(A)\times\mathrm{Dom}(B)\bigr)\cap F\ne\emptyset$, and similarly we have $(y,w)\in\bigl(\mathrm{Im}(A)\times\mathrm{Im}(B)\bigr)\cap G$.
On the other hand, suppose that for some $x,y,w,z\in S$ you have $(z,x)\in\bigl(\mathrm{Dom}(A)\times\mathrm{Dom}(B)\bigr)\cap F$ and $(y,w)\in\bigl(\mathrm{Im}(A)\times\mathrm{Im}(B)\bigr)\cap G$. Then for some $r,s,p,q\in S$ we have
$$zFx,\ zAr,\ xBs;\ yGw,\ pAy,\ qBw\,,$$
that is
$$xF^{-1}z,\ zAr,\ xBs;\ wG^{-1}y,\ pAy,\ qBw\,.$$
This implies that $(x,r)\in A\circ F^{-1}$ and $(q,b)\in G^{-1}\circ B$, and we are stuck at this point.
Finally, assume that $\bigl(\mathrm{Dom}(A)\times\mathrm{Im}(B)\bigr)\cap F\ne\emptyset$ and $\bigl(\mathrm{Dom}(A)\times\mathrm{Im}(B)\bigr)\cap G\ne\emptyset$. If $(z,x)\in\bigl(\mathrm{Dom}(A)\times\mathrm{Im}(B)\bigr)\cap F$ then for some $r,s\in S$ we have
$$zFx,\ zAr,\ sBx\,;$$
similarly, if $(y,w)\in\bigl(\mathrm{Dom}(A)\times\mathrm{Im}(B)\bigr)\cap G$ then for some $p,q\in S$ we have
$$yGw,\ yAp,\ qBw\,.$$
Consequently we have $(x,r)\in A\circ F^{-1}$ and $(q,y)\in G^{-1}\circ B$, and again we are unable to prove that the relations $A\circ F^{-1}$ and $G^{-1}\circ B$ do intersect.
It would be nice if you share your proof with us.
A: Let $x,y,z,w,p,q,r,s$ be distinct elements of a set $S$, and define
$$A=\bigl\{(z,r),(p,y)\bigr\},\ B=\bigl\{(x,s),(q,w)\bigr\},\ F=\bigl\{(z,x)\bigr\},\ G=\bigl\{(y,w)\bigr\}\,.$$
Then $\bigl[\mathrm{Dom}(A)\times\mathrm{Dom}(B)\bigr]\cap F=F\ne\emptyset, \bigl[\mathrm{Im}(A)\times\mathrm{Im}(B)\bigr]\cap G=G\ne\emptyset$, and yet $A\circ F^{-1}=\bigl\{(x,r)\bigr\}$ and $G^{-1}\circ B=\bigl\{(q,y)\bigr\}$, so $\bigr[A\circ F^{-1}\bigl]\cap\bigl[G^{-1}\circ B\bigr]=\emptyset$. I constructed this example based on my previous attempt to proving the equivalence. Thus, the implication
$$\Bigl[\bigl[\mathrm{Dom}(A)\times\mathrm{Dom}(B)\bigr]\cap F\ne\emptyset\ \wedge\ \bigl[\mathrm{Im}(A)\times\mathrm{Im}(B)\bigr]\cap G\ne\emptyset\Bigr]\Rightarrow\bigr[A\circ F^{-1}\bigl]\cap\bigl[G^{-1}\circ B\bigr]=\emptyset$$
is false, though the other implication is always true (as I proved in my previous comment/answer).
