I am stuck with a simple problem in mereology (the theory of parthood), where $P x y$ stands for $x$ is part of $y$ and $O x y$ stands for $x$ and $y$ overlap. From the axiom schema $(\exists x) \phi x \rightarrow (\exists z)(\forall y)(O y z \leftrightarrow (\phi x \wedge O y x))$, known as fusion or unrestricted composition, I am trying to derive the following, known as the sum and product axioms respectively:
$(\exists z) (Pxz \wedge Pyz) \rightarrow (\exists z) (\forall w)(O w z \leftrightarrow (O w x \vee O w y))$
$(\exists z) (Pzx \wedge Pzy) \rightarrow (\exists z) (\forall w) (P w z \leftrightarrow (Pwx \wedge Pwy))$.
I suppose it should be obvious, but what substitutions should I use for $\phi$?
It's assumed that $P$ is reflexive, antisymmetric and transitive, and that $O x y \leftrightarrow (\exists z)(P z x \wedge P z y)$. I shouldn't need to use the axiom of strong supplementation, $\neg P y x \to (\exists z) (P z y \wedge \neg O z x)$. But an answer which does use this axiom would be very helpful too.
The formulations are from Achille Varzi and Roberto Casati's Parts and Places (Cambridge, Mass: MIT Press, 1999), pp. 33-47. See also https://plato.stanford.edu/entries/mereology/