Wide pullbacks compute intersections of supplied set-indexed subobject representatives independently of the representatives

If $I=\mathrm{\varnothing }$, every subobject of $C$ factors through $1_C:C\to C$, so $1_C$ represents the greatest subobject of $C$; the empty family imposes no lower-bound condition, so $[1_C]$ is its greatest lower bound and hence its intersection by [L4].

Suppose $I$ is nonempty and write $p=m_i\circ p_i$, independent of $i$. If $p\circ x=p\circ y$, then monicity of every $m_i$ gives $p_i\circ x=p_i\circ y$ for all $i$, and joint monicity in [L3] gives $x=y$; hence $p$ is monic. Each equality $p=m_i{p}_i$ makes $[p]\le [m_i]$. If $q:Q\to C$ factors through every $m_i$, its factor maps form a cone and [L1] gives a unique $u:Q\to P$ with $q=p\circ u$, so $[q]\le [p]$. Thus [L4] makes $[p]$ the intersection.

By [L5], representatives of the same subobject mutually factor and their factor maps are unique inverse isomorphisms over $C$. Composing a wide-pullback cone with these isomorphisms gives a cone for the replacement family, and [L1] supplies mutually inverse comparison maps between the two pullback apices. Their induced monomorphisms into $C$ therefore mutually factor, so they represent the same intersection subobject.