Closed immersions are proper

Let $U=\mathrm{Spec}A$ be an affine open of $Y$. By [F1] and [F2] the restriction of $i$ over $U$ is a closed immersion with $i^{-1}(U)\cong \mathrm{Spec}(A\mathrm{/}I)$ over $U$ for the unique ideal $I\subseteq A$; in particular the inverse image is affine.

The quotient $A\mathrm{/}I$ is cyclic as an $A$-module: the class $1+I$ generates it, because every $a+I=a\cdot (1+I)$ lies in the submodule generated by $1+I$, while that submodule always lies in $A\mathrm{/}I$; if $I=A$ then $A\mathrm{/}I=0$ is generated by the empty family. Hence $A\mathrm{/}I$ is finitely generated, equivalently module-finite, over $A$ by [F4] and [F5].

Steps 1.1 and 1.2 verify the condition of [F3] on every affine open $U$ of $Y$: the inverse image is affine, $i^{-1}(U)=\mathrm{Spec}(A\mathrm{/}I)$, and its coordinate algebra is module-finite over the coordinate algebra of $U$. Therefore the closed immersion $i$ is finite.

By [F6] the finite morphism $i$ is proper. The empty closed immersion is included: over each affine $U=\mathrm{Spec}A$ it corresponds by [F2] to the ideal $I=A$, so its inverse image is $\mathrm{Spec}0$, an affine chart whose coordinate ring is the zero ring and is module-finite by [F3], and the same argument applies to it. The Axiom of Choice [F7] is assumed and is used only through [F2] and [F6], the two AC-qualified suppliers; no further selection occurs, and no Noetherian, reducedness or nonemptiness hypothesis is used.