[proofplan]
We construct a quasi-inverse $G:\mathcal{D}\to\mathcal{C}$ by choosing, for every object of $\mathcal{D}$, an object of $\mathcal{C}$ whose image under $F$ is isomorphic to it. Fullness and faithfulness then identify each morphism in $\mathcal{D}$ with a unique morphism in $\mathcal{C}$ between the chosen representatives. This uniqueness proves that $G$ preserves identities and composition. The chosen isomorphisms give $F G \cong \operatorname{id}_{\mathcal{D}}$, and full faithfulness gives the remaining natural isomorphism $\operatorname{id}_{\mathcal{C}} \cong G F$.
[/proofplan]
[step:Choose representatives for objects of $\mathcal{D}$]
Throughout the proof, for a category $\mathcal{E}$, the notation $\operatorname{Ob}(\mathcal{E})$ denotes the class of objects of $\mathcal{E}$. If $A,B\in\operatorname{Ob}(\mathcal{E})$, the notation $\operatorname{Hom}_{\mathcal{E}}(A,B)$ denotes the collection of morphisms in $\mathcal{E}$ with source $A$ and target $B$.
Since $F$ is essentially surjective on objects, for every object $D\in\operatorname{Ob}(\mathcal{D})$ there exist an object of $\mathcal{C}$ and an isomorphism from its image under $F$ to $D$. By the choice principle assumed in the statement, choose one such pair for each object $D$. Choose, for each $D\in\operatorname{Ob}(\mathcal{D})$, an object $G(D)\in\operatorname{Ob}(\mathcal{C})$ and an isomorphism
\begin{align*}
\varepsilon_D:F(G(D))\longrightarrow D
\end{align*}
in $\mathcal{D}$.
This defines the object function of a candidate functor
\begin{align*}
G:\mathcal{D}\longrightarrow\mathcal{C}.
\end{align*}
[guided]
For a category $\mathcal{E}$, the notation $\operatorname{Ob}(\mathcal{E})$ denotes the class of objects of $\mathcal{E}$. If $A,B\in\operatorname{Ob}(\mathcal{E})$, the notation $\operatorname{Hom}_{\mathcal{E}}(A,B)$ denotes the collection of morphisms in $\mathcal{E}$ with source $A$ and target $B$.
The hypothesis of essential surjectivity says exactly that every object of $\mathcal{D}$ is isomorphic to one lying in the image of $F$. We use this once, at the start, to choose a representative in $\mathcal{C}$ for each object of $\mathcal{D}$. The statement includes the needed choice principle, so we may make these choices simultaneously for all objects of $\mathcal{D}$.
Thus, for each object $D\in\operatorname{Ob}(\mathcal{D})$, choose an object $G(D)\in\operatorname{Ob}(\mathcal{C})$ and an isomorphism
\begin{align*}
\varepsilon_D:F(G(D))\longrightarrow D.
\end{align*}
The symbol $G(D)$ is the chosen representative of $D$ in $\mathcal{C}$, and $\varepsilon_D$ records that $F(G(D))$ is isomorphic to $D$ in $\mathcal{D}$. These choices define the object part of the desired quasi-inverse functor $G:\mathcal{D}\to\mathcal{C}$.
[/guided]
[/step]
[step:Define $G$ on morphisms using full faithfulness]
Let $D,D'\in\operatorname{Ob}(\mathcal{D})$, and let $u:D\to D'$ be a morphism in $\mathcal{D}$. The composite
\begin{align*}
\varepsilon_{D'}^{-1}\circ u\circ \varepsilon_D:F(G(D))\longrightarrow F(G(D'))
\end{align*}
is a morphism in $\mathcal{D}$. Since $F$ is full and faithful, the map
\begin{align*}
F_{G(D),G(D')}:\operatorname{Hom}_{\mathcal{C}}(G(D),G(D'))
&\longrightarrow
\operatorname{Hom}_{\mathcal{D}}(F(G(D)),F(G(D'))) \\
a&\longmapsto F(a)
\end{align*}
is bijective. Therefore there exists a unique morphism
\begin{align*}
G(u):G(D)\longrightarrow G(D')
\end{align*}
in $\mathcal{C}$ such that
\begin{align*}
F(G(u))=\varepsilon_{D'}^{-1}\circ u\circ \varepsilon_D.
\end{align*}
[guided]
We now define what $G$ does to a morphism. Let $u:D\to D'$ be a morphism in $\mathcal{D}$. Since $G(D)$ and $G(D')$ are only chosen representatives, the morphism $u$ does not directly have source and target $F(G(D))$ and $F(G(D'))$. The chosen isomorphisms transport $u$ to such a morphism:
\begin{align*}
\varepsilon_{D'}^{-1}\circ u\circ \varepsilon_D:F(G(D))\longrightarrow F(G(D')).
\end{align*}
The functor $F$ is full and faithful, so for the pair of objects $G(D),G(D')\in\operatorname{Ob}(\mathcal{C})$, the induced map
\begin{align*}
F_{G(D),G(D')}:\operatorname{Hom}_{\mathcal{C}}(G(D),G(D'))
&\longrightarrow
\operatorname{Hom}_{\mathcal{D}}(F(G(D)),F(G(D'))) \\
a&\longmapsto F(a)
\end{align*}
is bijective. Surjectivity gives existence of a morphism in $\mathcal{C}$ mapping to the transported morphism, and injectivity gives uniqueness. Define $G(u):G(D)\to G(D')$ to be the unique morphism satisfying
\begin{align*}
F(G(u))=\varepsilon_{D'}^{-1}\circ u\circ \varepsilon_D.
\end{align*}
This is the only possible definition compatible with the chosen isomorphisms $\varepsilon_D$.
[/guided]
[/step]
[step:Verify that $G$ preserves identities and composition]
Let $D\in\operatorname{Ob}(\mathcal{D})$. By the definition of $G$ on morphisms,
\begin{align*}
F(G(\operatorname{id}_D))
=
\varepsilon_D^{-1}\circ \operatorname{id}_D\circ \varepsilon_D
=
\operatorname{id}_{F(G(D))}
=
F(\operatorname{id}_{G(D)}).
\end{align*}
Since $F$ is faithful, $G(\operatorname{id}_D)=\operatorname{id}_{G(D)}$.
Now let
\begin{align*}
D\xrightarrow{u}D'\xrightarrow{v}D''
\end{align*}
be composable morphisms in $\mathcal{D}$. By the definition of $G$ on morphisms and functoriality of $F$,
\begin{align*}
F(G(v)\circ G(u))
&=
F(G(v))\circ F(G(u)) \\
&=
(\varepsilon_{D''}^{-1}\circ v\circ \varepsilon_{D'})
\circ
(\varepsilon_{D'}^{-1}\circ u\circ \varepsilon_D) \\
&=
\varepsilon_{D''}^{-1}\circ v\circ u\circ \varepsilon_D \\
&=
F(G(v\circ u)).
\end{align*}
Since $F$ is faithful, $G(v)\circ G(u)=G(v\circ u)$. Hence $G:\mathcal{D}\to\mathcal{C}$ is a functor.
[guided]
We must check that the morphism assignment just defined is functorial.
First let $D\in\operatorname{Ob}(\mathcal{D})$. Applying the definition of $G$ to the identity morphism $\operatorname{id}_D:D\to D$, we get
\begin{align*}
F(G(\operatorname{id}_D))
=
\varepsilon_D^{-1}\circ \operatorname{id}_D\circ \varepsilon_D.
\end{align*}
Since $\varepsilon_D$ is an isomorphism, the right-hand side is the identity morphism on $F(G(D))$:
\begin{align*}
F(G(\operatorname{id}_D))
=
\operatorname{id}_{F(G(D))}
=
F(\operatorname{id}_{G(D)}).
\end{align*}
Faithfulness means that $F$ is injective on each hom-set, so two morphisms in $\operatorname{Hom}_{\mathcal{C}}(G(D),G(D))$ with the same image under $F$ are equal. Therefore
\begin{align*}
G(\operatorname{id}_D)=\operatorname{id}_{G(D)}.
\end{align*}
Next let $D\xrightarrow{u}D'\xrightarrow{v}D''$ be composable morphisms in $\mathcal{D}$. We compare $G(v\circ u)$ and $G(v)\circ G(u)$ by applying $F$ to both. Since $F$ is a functor,
\begin{align*}
F(G(v)\circ G(u))
=
F(G(v))\circ F(G(u)).
\end{align*}
Using the defining formula for $G(u)$ and $G(v)$ gives
\begin{align*}
F(G(v)\circ G(u))
&=
(\varepsilon_{D''}^{-1}\circ v\circ \varepsilon_{D'})
\circ
(\varepsilon_{D'}^{-1}\circ u\circ \varepsilon_D) \\
&=
\varepsilon_{D''}^{-1}\circ v\circ u\circ \varepsilon_D.
\end{align*}
The middle factors $\varepsilon_{D'}\circ\varepsilon_{D'}^{-1}$ cancel because $\varepsilon_{D'}$ is an isomorphism. By the definition of $G(v\circ u)$, the same morphism is
\begin{align*}
F(G(v\circ u))
=
\varepsilon_{D''}^{-1}\circ (v\circ u)\circ \varepsilon_D.
\end{align*}
Thus $F(G(v)\circ G(u))=F(G(v\circ u))$. Faithfulness of $F$ gives
\begin{align*}
G(v)\circ G(u)=G(v\circ u).
\end{align*}
Together with preservation of identities, this proves that $G:\mathcal{D}\to\mathcal{C}$ is a functor.
[/guided]
[/step]
[step:Assemble the chosen isomorphisms into a natural isomorphism $F G\cong \operatorname{id}_{\mathcal{D}}$]
For each object $D\in\operatorname{Ob}(\mathcal{D})$, the morphism
\begin{align*}
\varepsilon_D:F(G(D))\longrightarrow D
\end{align*}
is an isomorphism by construction. We verify naturality. Let $u:D\to D'$ be a morphism in $\mathcal{D}$. From the defining equation for $G(u)$,
\begin{align*}
F(G(u))=\varepsilon_{D'}^{-1}\circ u\circ \varepsilon_D.
\end{align*}
Composing on the left by $\varepsilon_{D'}$ gives
\begin{align*}
\varepsilon_{D'}\circ F(G(u))
=
u\circ \varepsilon_D.
\end{align*}
Thus the square
\begin{align*}
F(G(D)) &\xrightarrow{F(G(u))} F(G(D')) \\
\varepsilon_D \downarrow \phantom{\varepsilon_D} & \phantom{\varepsilon_{D'}} \downarrow \varepsilon_{D'} \\
D &\xrightarrow{u} D'
\end{align*}
commutes. Therefore $\varepsilon:F\circ G\Longrightarrow \operatorname{id}_{\mathcal{D}}$ is a natural isomorphism.
[guided]
For each object $D\in\operatorname{Ob}(\mathcal{D})$, we already chose an isomorphism
\begin{align*}
\varepsilon_D:F(G(D))\longrightarrow D.
\end{align*}
To show that these components form a natural transformation $\varepsilon:F\circ G\Longrightarrow \operatorname{id}_{\mathcal{D}}$, we must prove naturality for every morphism $u:D\to D'$ in $\mathcal{D}$.
The definition of $G(u)$ was chosen precisely so that
\begin{align*}
F(G(u))=\varepsilon_{D'}^{-1}\circ u\circ \varepsilon_D.
\end{align*}
Composing this equality on the left by the isomorphism $\varepsilon_{D'}$ gives
\begin{align*}
\varepsilon_{D'}\circ F(G(u))
&=
\varepsilon_{D'}\circ \varepsilon_{D'}^{-1}\circ u\circ \varepsilon_D \\
&=
u\circ \varepsilon_D,
\end{align*}
where the symbol $\nu$ denotes the morphism $u:D\to D'$ under discussion. Equivalently, replacing $\nu$ by $u$,
\begin{align*}
\varepsilon_{D'}\circ F(G(u))
=
u\circ \varepsilon_D
=
u\circ \varepsilon_D.
\end{align*}
Thus the naturality square
\begin{align*}
F(G(D)) &\xrightarrow{F(G(u))} F(G(D')) \\
\varepsilon_D \downarrow \phantom{\varepsilon_D} & \phantom{\varepsilon_{D'}} \downarrow \varepsilon_{D'} \\
D &\xrightarrow{u} D'
\end{align*}
commutes for every morphism $u:D\to D'$. Since each component $\varepsilon_D$ is an isomorphism by construction, $\varepsilon:F\circ G\Longrightarrow \operatorname{id}_{\mathcal{D}}$ is a natural isomorphism.
[/guided]
[/step]
[step:Construct the natural isomorphism $\operatorname{id}_{\mathcal{C}}\cong G F$]
Let $C\in\operatorname{Ob}(\mathcal{C})$. Since $F$ is full and faithful, the map
\begin{align*}
F_{C,G(F(C))}:\operatorname{Hom}_{\mathcal{C}}(C,G(F(C)))
&\longrightarrow
\operatorname{Hom}_{\mathcal{D}}(F(C),F(G(F(C)))) \\
a&\longmapsto F(a)
\end{align*}
is bijective. Define
\begin{align*}
\eta_C:C\longrightarrow G(F(C))
\end{align*}
to be the unique morphism satisfying
\begin{align*}
F(\eta_C)=\varepsilon_{F(C)}^{-1}:F(C)\longrightarrow F(G(F(C))).
\end{align*}
Because $\varepsilon_{F(C)}^{-1}$ is an isomorphism, let $\theta_C:G(F(C))\to C$ be the unique morphism satisfying
\begin{align*}
F(\theta_C)=\varepsilon_{F(C)}.
\end{align*}
Existence and uniqueness of $\theta_C$ follow from the bijectivity of the full and faithful map $F_{G(F(C)),C}$. Then
\begin{align*}
F(\theta_C\circ \eta_C)
&=
F(\theta_C)\circ F(\eta_C) \\
&=
\varepsilon_{F(C)}\circ \varepsilon_{F(C)}^{-1} \\
&=
\operatorname{id}_{F(C)}
=
F(\operatorname{id}_C),
\end{align*}
and faithfulness gives $\theta_C\circ\eta_C=\operatorname{id}_C$. Similarly,
\begin{align*}
F(\eta_C\circ \theta_C)
&=
F(\eta_C)\circ F(\theta_C) \\
&=
\varepsilon_{F(C)}^{-1}\circ \varepsilon_{F(C)} \\
&=
\operatorname{id}_{F(G(F(C)))}
=
F(\operatorname{id}_{G(F(C))}),
\end{align*}
so faithfulness gives $\eta_C\circ\theta_C=\operatorname{id}_{G(F(C))}$. Hence $\eta_C$ is an isomorphism.
We verify naturality. Let $f:C\to C'$ be a morphism in $\mathcal{C}$. Applying $F$ to the two composites gives
\begin{align*}
F(G(F(f))\circ \eta_C)
&=
F(G(F(f)))\circ F(\eta_C) \\
&=
(\varepsilon_{F(C')}^{-1}\circ F(f)\circ \varepsilon_{F(C)})
\circ
\varepsilon_{F(C)}^{-1} \\
&=
\varepsilon_{F(C')}^{-1}\circ F(f),
\end{align*}
while
\begin{align*}
F(\eta_{C'}\circ f)
=
F(\eta_{C'})\circ F(f)
=
\varepsilon_{F(C')}^{-1}\circ F(f).
\end{align*}
Faithfulness of $F$ gives
\begin{align*}
G(F(f))\circ \eta_C=\eta_{C'}\circ f.
\end{align*}
Thus $\eta:\operatorname{id}_{\mathcal{C}}\Longrightarrow G\circ F$ is a natural isomorphism.
[guided]
The first natural isomorphism came directly from the choices $\varepsilon_D$. The second one must be extracted from full faithfulness.
Fix an object $C\in\operatorname{Ob}(\mathcal{C})$. We need an isomorphism from $C$ to $G(F(C))$. After applying $F$, such a morphism should become a morphism
\begin{align*}
F(C)\longrightarrow F(G(F(C))).
\end{align*}
But we already have the chosen isomorphism
\begin{align*}
\varepsilon_{F(C)}:F(G(F(C)))\longrightarrow F(C),
\end{align*}
so its inverse has exactly the right source and target:
\begin{align*}
\varepsilon_{F(C)}^{-1}:F(C)\longrightarrow F(G(F(C))).
\end{align*}
Since $F$ is full and faithful, the map
\begin{align*}
F_{C,G(F(C))}:\operatorname{Hom}_{\mathcal{C}}(C,G(F(C)))
&\longrightarrow
\operatorname{Hom}_{\mathcal{D}}(F(C),F(G(F(C)))) \\
a&\longmapsto F(a)
\end{align*}
is bijective. Therefore there is a unique morphism
\begin{align*}
\eta_C:C\longrightarrow G(F(C))
\end{align*}
such that
\begin{align*}
F(\eta_C)=\varepsilon_{F(C)}^{-1}.
\end{align*}
This morphism is an isomorphism. Indeed, because $\varepsilon_{F(C)}^{-1}$ is an isomorphism in $\mathcal{D}$, let
\begin{align*}
b:F(G(F(C)))\longrightarrow F(C)
\end{align*}
be its inverse, so $b=\varepsilon_{F(C)}$. By fullness, there exists a morphism
\begin{align*}
\theta_C:G(F(C))\longrightarrow C
\end{align*}
such that $F(\theta_C)=\varepsilon_{F(C)}$. Then
\begin{align*}
F(\theta_C\circ \eta_C)
&=
F(\theta_C)\circ F(\eta_C) \\
&=
\varepsilon_{F(C)}\circ \varepsilon_{F(C)}^{-1} \\
&=
\operatorname{id}_{F(C)}
=
F(\operatorname{id}_C),
\end{align*}
and faithfulness gives $\theta_C\circ\eta_C=\operatorname{id}_C$. Similarly,
\begin{align*}
F(\eta_C\circ \theta_C)
&=
F(\eta_C)\circ F(\theta_C) \\
&=
\varepsilon_{F(C)}^{-1}\circ \varepsilon_{F(C)} \\
&=
\operatorname{id}_{F(G(F(C)))}
=
F(\operatorname{id}_{G(F(C))}),
\end{align*}
so faithfulness gives $\eta_C\circ\theta_C=\operatorname{id}_{G(F(C))}$. Hence $\eta_C$ is an isomorphism.
It remains to check naturality. Let $f:C\to C'$ be a morphism in $\mathcal{C}$. The naturality square for $\eta$ asks for
\begin{align*}
G(F(f))\circ \eta_C=\eta_{C'}\circ f.
\end{align*}
We prove this equality by applying $F$ and then using faithfulness. The definition of $G$ applied to the morphism $F(f):F(C)\to F(C')$ gives
\begin{align*}
F(G(F(f)))
=
\varepsilon_{F(C')}^{-1}\circ F(f)\circ \varepsilon_{F(C)}.
\end{align*}
Therefore
\begin{align*}
F(G(F(f))\circ \eta_C)
&=
F(G(F(f)))\circ F(\eta_C) \\
&=
(\varepsilon_{F(C')}^{-1}\circ F(f)\circ \varepsilon_{F(C)})
\circ
\varepsilon_{F(C)}^{-1} \\
&=
\varepsilon_{F(C')}^{-1}\circ F(f).
\end{align*}
On the other hand,
\begin{align*}
F(\eta_{C'}\circ f)
=
F(\eta_{C'})\circ F(f)
=
\varepsilon_{F(C')}^{-1}\circ F(f).
\end{align*}
The two images under $F$ are equal, and both original morphisms have source $C$ and target $G(F(C'))$. Since $F$ is faithful, the original morphisms are equal:
\begin{align*}
G(F(f))\circ \eta_C=\eta_{C'}\circ f.
\end{align*}
Thus $\eta:\operatorname{id}_{\mathcal{C}}\Longrightarrow G\circ F$ is a natural isomorphism.
[/guided]
[/step]
[step:Conclude that $F$ is an equivalence of categories]
We have constructed a functor
\begin{align*}
G:\mathcal{D}\longrightarrow\mathcal{C}
\end{align*}
and natural isomorphisms
\begin{align*}
\varepsilon:F\circ G\Longrightarrow \operatorname{id}_{\mathcal{D}},
\qquad
\eta:\operatorname{id}_{\mathcal{C}}\Longrightarrow G\circ F.
\end{align*}
Therefore $G$ is a quasi-inverse to $F$, and hence $F$ is an equivalence of categories.
[guided]
The definition of equivalence of categories requires a functor in the opposite direction and natural isomorphisms from both composites to the corresponding identity functors. We have constructed the functor
\begin{align*}
G:\mathcal{D}\longrightarrow\mathcal{C}
\end{align*}
and proved that the chosen isomorphisms assemble into a natural isomorphism
\begin{align*}
\varepsilon:F\circ G\Longrightarrow \operatorname{id}_{\mathcal{D}}.
\end{align*}
We also constructed, using full faithfulness, a natural isomorphism
\begin{align*}
\eta:\operatorname{id}_{\mathcal{C}}\Longrightarrow G\circ F.
\end{align*}
Thus $G$ is a quasi-inverse functor to $F$. By the definition of equivalence of categories, $F$ is an equivalence of categories.
[/guided]
[/step]
