@Matthew – I think there's a typo in your (4):

> 4: \$$\Phi(-, y) : \mathcal{X}^{\mathrm{op}} \Rightarrow \mathcal{V}\$$ and \$$\Phi(x, -) : \mathcal{Y} \Rightarrow \mathcal{V}\$$ are both \$$\mathcal{V}\$$-profunctors for all \$$x,y\$$

because what you've proved is

> 4: \$$\Phi(-, y) : \mathcal{X}^{\mathrm{op}} \rightarrow \mathcal{V}\$$ and \$$\Phi(x, -) : \mathcal{Y} \rightarrow \mathcal{V}\$$ are both \$$\mathcal{V}\$$-functors for all \$$x,y\$$

fwiw the Yoneda lemma has always puzzled me because it seems to rely on some trick involving "special" properties of **Set** (in particular the role **Set** plays in defining "plain vanilla" categories). I once asked a category theoretician friend of mine what this "special" was exactly, and he replied "symmetric monoidal closed". Anyway, I think I'm getting reasonably close to understanding his answer, albeit over a decade later.