For any sets $X$ and $Y$, let $Y^X$ denote the set of all functions with domain $X$ and image contained in $Y$.¹

Let sets $A$ and $B$ be given.

For sets $Q$ and functions $q_A$ and $q_B$, we define the predicate

$\mathtt{Compatible}_{A,B}(Q,q_A,q_B)$: $q_A \in A^Q$ and $q_B \in B^Q$.

If $\mathtt{Compatible}_{A,B}(P,p_A,p_B)$ is true, define the predicate

$\mathtt{Prod}_{A,B}(P,p_A,p_B)$: If $\mathtt{Compatible}_{A,B}(Q,q_A,q_B)$ is true, then there exists a unique function $f \in P^Q$ such that $p_A \circ f = q_A$ and $p_B \circ f = q_B$.

Theorem

If $\mathtt{Prod}_{A,B}(P,p_A,p_B)$ is true and $\mathtt{Prod}_{A,B}(Q,q_A,q_B)$ is true, then there is a bijection $P \to Q$.

Proof

Because $\mathtt{Prod}_{A,B}(P,p_A,p_B)$ is true and $\mathtt{Compatible}_{A,B}(Q,q_A,q_B)$ is true, there is a unique function $f \in P^Q$ such that $$ \begin{equation} p_A \circ f = q_A \label{qA} \end{equation} $$ and $$ \begin{equation} \quad p_B \circ f = q_B. \label{qB} \end{equation} $$

Because $\mathtt{Prod}_{A,B}(Q,q_A,q_B)$ is true and $\mathtt{Compatible}_{A,B}(P,p_A,p_B)$ is true, there is a unique function $g \in Q^P$ such that $$ \begin{equation} q_A \circ g = p_A \label{pA} \end{equation} $$ and $$ \begin{equation} \quad q_B \circ g = p_B. \label{pB} \end{equation} $$

From $f \in P^Q$ and $g \in Q^P$, it follows that $f \circ g \in P^P$. Define $$\phi = f \circ g, \qquad \phi \in P^P.$$

From $\phi \in P^P$ and $p_A \in A^P$, it follows that $p_A \circ \phi \in A^P$. From $\phi \in P^P$ and $p_B \in B^P$, it follows that $p_B \circ \phi \in B^P$. Therefore, $\mathtt{Compatible}_{A,B}(P,p_A \circ \phi,p_B \circ \phi)$ is true.

Because $\mathtt{Prod}_{A,B}(P,p_A,p_B)$ is true and $\mathtt{Compatible}_{A,B}(P,p_A \circ \phi,p_B \circ \phi)$ is true, there is a unique function $h \in P^P$ such that $$ \begin{equation} p_A \circ h = p_A \circ \phi \label{pAphi} \end{equation} $$ and $$ \begin{equation} p_B \circ h = p_B \circ \phi. \label{pBphi} \end{equation} $$

But $$ \begin{align*} p_A \circ \phi&= p_A \circ (f \circ g)\\ &=(p_A \circ f) \circ g \quad \textrm{by associativity}\\ &=q_A \circ g \quad \textrm{by \eqref{qA}}\\ &=p_A \quad \textrm{by \eqref{pA}} \end{align*} $$ and $$ \begin{align*} p_B \circ \phi&=p_B \circ (f \circ g)\\ &=(p_B \circ f) \circ g \quad \textrm{by associativity}\\ &=q_B \circ g \quad \textrm{by \eqref{qB}}\\ &=p_B \quad \textrm{by \eqref{pB}}. \end{align*} $$

Thus $\eqref{pAphi}$ is equivalent with $$ p_A \circ h = p_A $$ and $\eqref{pBphi}$ is equivalent with $$ p_B \circ h = p_B. $$

Thus, $\textrm{id}_P \in P^P$ satisfies $\eqref{pAphi}$ and $\eqref{pBphi}$. Because $h$ is the unique element of $P^P$ satsifying $\eqref{pAphi}$ and $\eqref{pBphi}$, it follows that $$h=\textrm{id}_P.$$

From $g \in Q^P$ and $f \in P^Q$, it follows that $g \circ f \in Q^Q$. Define $$\psi = g \circ f, \qquad \psi \in Q^Q.$$

From $\psi \in Q^Q$ and $q_A \in A^Q$, it follows that $q_A \circ \psi \in A^Q$. From $\psi \in Q^Q$ and $q_B \in B^Q$, it follows that $q_B \circ \psi \in B^Q$. Therefore, $\mathtt{Compatible}_{A,B}(Q,q_A \circ \psi,q_B \circ \psi)$ is true.

Because $\mathtt{Prod}_{A,B}(Q,q_A,q_B)$ is true and $\mathtt{Compatible}_{A,B}(Q,q_A \circ \psi,q_B \circ \psi)$ is true, there is a unique function $k \in Q^Q$ such that $$ \begin{equation} q_A \circ k = q_A \circ \psi \label{qApsi} \end{equation} $$ and $$ \begin{equation} q_B \circ k = q_B \circ \psi. \label{qBpsi} \end{equation} $$

But $$ \begin{align*} q_A \circ \psi&=q_A \circ (g \circ f)\\ &=(q_A \circ g) \circ f \quad \textrm{by associativity}\\ &=p_A \circ f \quad \textrm{by \eqref{pA}}\\ &=q_A \quad \textrm{by \eqref{qA}} \end{align*} $$ and $$ \begin{align*} q_B \circ \psi&=q_B \circ (g \circ f)\\ &=(q_B \circ g) \circ f \quad \textrm{by associativity}\\ &=p_B \circ f \quad \textrm{by \eqref{pB}}\\ &=q_B \quad \textrm{by \eqref{qB}}. \end{align*} $$

Thus $\eqref{qApsi}$ is equivalent with $$ q_A \circ k = q_A $$ and $\eqref{qBpsi}$ is equivalent with $$ q_B \circ k = q_B. $$

Thus, $\textrm{id}_Q \in Q^Q$ satisfies $\eqref{qApsi}$ and $\eqref{qBpsi}$. Because $k$ is the unique element of $Q^Q$ satsifying $\eqref{qApsi}$ and $\eqref{qBpsi}$, it follows that $$k=\textrm{id}_Q.$$

∎

References² ³

Indeed, this makes sense when one or both of $X$ or $Y$ is the empty set. ↩
Category Theory: a concise course. 5. Product, Coproduct, Exponential | Charlotte Aten, Venanzio Capretta, and William DeMeo ↩
Product is unique up to isomorphism | Arbital ↩