[000Y] Lemma 5.2·d.

The externalization [000V] is locally small

Proof. Fix $x\in E$ and $u,v\in \brk{C}\Sub{x}$, we must exhibit a terminal object to the (total) category $\TotCat{\CandHom{x}{u}{v}}$ of “hom candidates” defined in [000I]. First we define $\brk{u,v}$ to be the following pullback in $E$:

We define $\overline{p}:\InvImg{\brk{u,v}}{u}\to\Sub{p} u\in \brk{C}\Sub{\brk{u,v}}$ to be the cartesian lift of $u\in \brk{C}\Sub{x}$ along $p:\brk{u,v}\to x$:

We need to define a displayed evaluation map $\epsilon : \InvImg{\brk{u,v}}u\to\Sub{p} v$; unraveling the definition of a displayed morphism in the externalization of $C$, we choose the following diagram:

Putting all this together, we assert that the terminal object of $\TotCat{\CandHom{x}{u}{v}}$ is the following span in $\brk{C}$:

Fixing another such candidate hom span $\brc{u \leftarrow \bar{h}\rightarrow v}\in\TotCat{\CandHom{x}{u}{v}}$, according to [000I] we must exhibit a unique cartesian morphism $\bar\alpha : \bar{h}\to \InvImg{\brk{u,v}}{u}$ making the following diagram commute:

First we note that the evaluation map $\epsilon\Sub{h} : \bar{h}\to v$ amounts to an internal morphism $h\to C\Sub{1}$ satisfying the appropriate compatibility conditions. Therefore we may define the base $\alpha:h\to \brk{u,v}$ of the universal map using the universal property of the pullback that defines $\brk{u,v}$:

The morphism $\alpha:h\to \brk{u,v}$ defined above is the unique map in $E$ satisfying the conditions required of the base for $\bar\alpha$; therefore, it suffices to show that there exists a cartesian morphism $\bar\alpha:\bar{h}\to\Sub{\alpha}\InvImg{\brk{u,v}}u$ since it will be unique if it exists. We define $\bar\alpha$ using the universal property of the cartesian lift:

That $\bar{\alpha}:\bar{h}\to\Sub{\alpha}\InvImg{\brk{u,v}}u$ is cartesian follows from the “generalized pullback lemma” for cartesian morphisms [0014]: it suffices to observe that both $\bar{p}\Sub{h}:\bar{h}\to u$ and its second factor $\bar{p}:\InvImg{\brk{u,v}}u\to u$ are cartesian.