[proofplan]
The objects, morphisms, identity morphisms, and composition law of $\mathcal C^{\mathrm{op}}$ have been specified, so it remains to verify the category axioms. Associativity in $\mathcal C^{\mathrm{op}}$ follows by translating a triple composite into $\mathcal C$, where the order of composition is reversed and associativity is already known. The identity laws follow because the identity morphism at each object is the same underlying morphism as in $\mathcal C$.
[/proofplan]
[step:Verify that the reversed composition is well-defined]
Let $A,B,D\in \operatorname{Ob}(\mathcal C^{\mathrm{op}})$. Let
\begin{align*}
f\in \operatorname{Hom}_{\mathcal C^{\mathrm{op}}}(A,B),
\qquad
g\in \operatorname{Hom}_{\mathcal C^{\mathrm{op}}}(B,D).
\end{align*}
By the definition of the morphism sets in $\mathcal C^{\mathrm{op}}$, these same symbols denote morphisms
\begin{align*}
f\in \operatorname{Hom}_{\mathcal C}(B,A),
\qquad
g\in \operatorname{Hom}_{\mathcal C}(D,B).
\end{align*}
Therefore $f\circ_{\mathcal C} g$ is defined in $\mathcal C$ and belongs to $\operatorname{Hom}_{\mathcal C}(D,A)$. Since
\begin{align*}
\operatorname{Hom}_{\mathcal C^{\mathrm{op}}}(A,D)=\operatorname{Hom}_{\mathcal C}(D,A),
\end{align*}
the morphism $g\circ_{\mathcal C^{\mathrm{op}}} f:=f\circ_{\mathcal C} g$ belongs to $\operatorname{Hom}_{\mathcal C^{\mathrm{op}}}(A,D)$. Hence composition in $\mathcal C^{\mathrm{op}}$ is well-defined.
[/step]
[step:Prove associativity by translating the composite into $\mathcal C$]
Let $A,B,D,E\in \operatorname{Ob}(\mathcal C^{\mathrm{op}})$, and let
\begin{align*}
f\in \operatorname{Hom}_{\mathcal C^{\mathrm{op}}}(A,B),\qquad
g\in \operatorname{Hom}_{\mathcal C^{\mathrm{op}}}(B,D),\qquad
h\in \operatorname{Hom}_{\mathcal C^{\mathrm{op}}}(D,E).
\end{align*}
Equivalently, in $\mathcal C$,
\begin{align*}
f\in \operatorname{Hom}_{\mathcal C}(B,A),\qquad
g\in \operatorname{Hom}_{\mathcal C}(D,B),\qquad
h\in \operatorname{Hom}_{\mathcal C}(E,D).
\end{align*}
Using the definition of composition in $\mathcal C^{\mathrm{op}}$ twice, we obtain
\begin{align*}
h\circ_{\mathcal C^{\mathrm{op}}}(g\circ_{\mathcal C^{\mathrm{op}}} f)
&= (g\circ_{\mathcal C^{\mathrm{op}}} f)\circ_{\mathcal C} h \\
&= (f\circ_{\mathcal C} g)\circ_{\mathcal C} h.
\end{align*}
Similarly,
\begin{align*}
(h\circ_{\mathcal C^{\mathrm{op}}} g)\circ_{\mathcal C^{\mathrm{op}}} f
&= f\circ_{\mathcal C}(h\circ_{\mathcal C^{\mathrm{op}}} g) \\
&= f\circ_{\mathcal C}(g\circ_{\mathcal C} h).
\end{align*}
Since $\mathcal C$ is a category, composition in $\mathcal C$ is associative, so
\begin{align*}
(f\circ_{\mathcal C} g)\circ_{\mathcal C} h
=
f\circ_{\mathcal C}(g\circ_{\mathcal C} h).
\end{align*}
Therefore
\begin{align*}
h\circ_{\mathcal C^{\mathrm{op}}}(g\circ_{\mathcal C^{\mathrm{op}}} f)
=
(h\circ_{\mathcal C^{\mathrm{op}}} g)\circ_{\mathcal C^{\mathrm{op}}} f.
\end{align*}
Thus composition in $\mathcal C^{\mathrm{op}}$ is associative.
[/step]
[step:Prove the identity laws using the identities of $\mathcal C$]
Let $A,B\in \operatorname{Ob}(\mathcal C^{\mathrm{op}})$ and let
\begin{align*}
f\in \operatorname{Hom}_{\mathcal C^{\mathrm{op}}}(A,B).
\end{align*}
Then $f\in \operatorname{Hom}_{\mathcal C}(B,A)$. By definition,
\begin{align*}
\operatorname{id}^{\mathcal C^{\mathrm{op}}}_A=\operatorname{id}^{\mathcal C}_A,
\qquad
\operatorname{id}^{\mathcal C^{\mathrm{op}}}_B=\operatorname{id}^{\mathcal C}_B.
\end{align*}
For the left identity law in $\mathcal C^{\mathrm{op}}$, the reversed composition rule gives
\begin{align*}
f\circ_{\mathcal C^{\mathrm{op}}}\operatorname{id}^{\mathcal C^{\mathrm{op}}}_A
=
\operatorname{id}^{\mathcal C}_A\circ_{\mathcal C} f.
\end{align*}
Since $\operatorname{id}^{\mathcal C}_A$ is the identity morphism at $A$ in $\mathcal C$ and $f:B\to A$ in $\mathcal C$, the right identity law in $\mathcal C$ gives
\begin{align*}
\operatorname{id}^{\mathcal C}_A\circ_{\mathcal C} f=f.
\end{align*}
Thus
\begin{align*}
f\circ_{\mathcal C^{\mathrm{op}}}\operatorname{id}^{\mathcal C^{\mathrm{op}}}_A=f.
\end{align*}
For the right identity law in $\mathcal C^{\mathrm{op}}$, the reversed composition rule gives
\begin{align*}
\operatorname{id}^{\mathcal C^{\mathrm{op}}}_B\circ_{\mathcal C^{\mathrm{op}}} f
=
f\circ_{\mathcal C}\operatorname{id}^{\mathcal C}_B.
\end{align*}
Since $\operatorname{id}^{\mathcal C}_B$ is the identity morphism at $B$ in $\mathcal C$ and $f:B\to A$ in $\mathcal C$, the left identity law in $\mathcal C$ gives
\begin{align*}
f\circ_{\mathcal C}\operatorname{id}^{\mathcal C}_B=f.
\end{align*}
Therefore
\begin{align*}
\operatorname{id}^{\mathcal C^{\mathrm{op}}}_B\circ_{\mathcal C^{\mathrm{op}}} f=f.
\end{align*}
Both identity laws hold in $\mathcal C^{\mathrm{op}}$.
[/step]
[step:Conclude that all category axioms hold]
The composition operation in $\mathcal C^{\mathrm{op}}$ is well-defined, associative, and has identity morphisms $\operatorname{id}^{\mathcal C^{\mathrm{op}}}_A$ for every object $A\in \operatorname{Ob}(\mathcal C^{\mathrm{op}})$. Hence $\mathcal C^{\mathrm{op}}$ satisfies the axioms of a category.
[/step]
