A complete locally small category with a small coseparating set and intersections of all subobject collections has an initial object

Form the set-indexed product $P={\prod }_{K\in \mathrm{\Phi }}K$. By the Statement's hypothesis in the sense recorded in [L4], the collection of all subobjects of $P$, possibly a proper collection, has an intersection $i:I\to P$. This invokes that order-theoretic greatest lower bound directly and does not form a proper-class diagram.

Fix an object $C$. By [L2], the canonical evaluation map ${\nu }_C:C\to {\prod }_{K\in \mathrm{\Phi }}{\prod }_{f\in \mathcal{C}(C,K)}K$ is a set-indexed product map, and [L3] makes it monic. Repeating each projection of $P$ defines $\mathrm{\Delta }:P\to {\prod }_{K\in \mathrm{\Phi }}{\prod }_{f\in \mathcal{C}(C,K)}K$. Pull back ${\nu }_C$ along $\mathrm{\Delta }$ to obtain $P_C\to P$ with a map $P_C\to C$; that pullback of the monomorphism ${\nu }_C$ is monic by [L7], so $P_C\to P$ is a subobject of $P$. Since $i$ lies below every subobject of $P$, [L4] gives $I\to P_C$, hence a map $I\to C$.

If $f,g:I\rightrightarrows C$, their equalizer $e:E\to I$ is monic by [L5], and the composite $i\circ e:E\to P$ is monic by [L6], hence a subobject of $P$. Minimality of $i$ gives a factorisation $I\to E$ over $P$, so $e$ and $1_I$ — the latter monic by [L6] — represent the same subobject and $e$ is invertible. Therefore $f=g$. Step 2.1 gives existence and this step gives uniqueness for every target, so $I$ is initial.