Finite-dimensional projective space is proper over every base

By [F3] the morphism $\pi$ is of finite type, hence by [F4] it is locally of finite type and quasi-compact, and by [F2] it is separated.

Let a valuative diagram for $\pi$ be given: a valuation ring $R\subseteq K$ with fraction field $K$, morphisms $a:\mathrm{Spec}K\to {\mathbb{P}}_S^n$ and $b:\mathrm{Spec}R\to S$, and $j:\mathrm{Spec}K\to \mathrm{Spec}R$ with $\pi \circ a=b\circ j$ [F6]. Let $s_R\in \mathrm{Spec}R$ be the point corresponding to the unique maximal ideal of $R$, which exists by [F7]. For every $\mathfrak{p}\in \mathrm{Spec}R$ we have $\mathfrak{p}\subseteq {\mathfrak{m}}_R$, so $s_R$ is a specialization of $\mathfrak{p}$ by [F14]. Continuity of $b$ [F15] shows that $b(s_R)$ is a specialization of $b(\mathfrak{p})$. Choose an affine open $V=\mathrm{Spec}A\subseteq S$ containing $b(s_R)$ [F8]. Since $V$ is open and contains the specialization $b(s_R)$, it contains every generalization $b(\mathfrak{p})$: otherwise its closed complement would contain $b(\mathfrak{p})$ and hence its closure, including $b(s_R)$. Thus the image of $b$ lies in $V$ and $b$ factors through $V$ [F9]. Since $\pi (a(\eta ))=b(j(\eta ))\in V$, the map $a$ factors through the open subscheme ${\pi }^{-1}(V)={\mathbb{P}}_A^n\subseteq {\mathbb{P}}_S^n$ [F1, F9]. Replacing $S$ by $V$, it suffices to construct a lift over the affine base $A$; when $S=\mathrm{\varnothing }$ there is no morphism $\mathrm{Spec}R\to S$ at all, so assume from here on that the diagram exists.

Over the affine base the charts $U_i^A=\mathrm{Spec}A[x_{\mathrm{\ell }}^{(i)}:\mathrm{\ell }\mathrm{\ne }i]$, $i=0,\dots ,n$, form an open cover of ${\mathbb{P}}_A^n$ [F1], so the point $a(\eta )$ lies in some chart $U_i^A$, which we fix; then $a$ factors through $U_i^A$ [F9]. By [F10] the morphism from $\mathrm{Spec}K$ to the affine chart $U_i^A$ corresponds to an $A$-algebra homomorphism $\psi :A[x_{\mathrm{\ell }}^{(i)}:\mathrm{\ell }\mathrm{\ne }i]\to K$. Put $a_{\mathrm{\ell }}:=\psi (x_{\mathrm{\ell }}^{(i)})\in K$ for $\mathrm{\ell }\mathrm{\ne }i$ and $a_i:=1\in K$.

The tuple $a_0,\dots ,a_n$ has $a_i=1$, so some entry is nonzero. We claim that there is an index $m$ with $a_m\mathrm{\ne }0$ and $a_j\mathrm{/}{a}_m\in R$ for every $j$. Start with $m:=i$ and process the indices $j\mathrm{\ne }i$ one at a time, maintaining the invariant that $a_m\mathrm{\ne }0$ and $a_{j^{\mathrm{\prime }}}\mathrm{/}{a}_m\in R$ for every already processed $j^{\mathrm{\prime }}$. If $a_j=0$, then $a_j\mathrm{/}{a}_m=0\in R$ and $m$ is kept. If $a_j\mathrm{\ne }0$, apply [F7] to $x=a_j\mathrm{/}{a}_m\in K^{\times }$: either $a_j\mathrm{/}{a}_m\in R$, and $m$ is kept, or $a_m\mathrm{/}{a}_j\in R$, and we replace $m$ by $j$; in the second case $a_{j^{\mathrm{\prime }}}\mathrm{/}{a}_j=(a_{j^{\mathrm{\prime }}}\mathrm{/}{a}_m)(a_m\mathrm{/}{a}_j)\in R$ for every processed $j^{\mathrm{\prime }}$, so the invariant is preserved. At the end $a_j\mathrm{/}{a}_m\in R$ for all $j$, as claimed.

Since $a_m=\psi (x_m^{(i)})\mathrm{\ne }0$, the point $a(\eta )$ lies in the distinguished open $D(x_m^{(i)})=U_i^A\cap U_m^A$ [F1], so $a$ factors through the open subscheme $U_m^A$ [F9]. By the transition formula $x_{\mathrm{\ell }}^{(m)}=x_{\mathrm{\ell }}^{(i)}\mathrm{/}{x}_m^{(i)}$ of [F1], the restriction of $a$ to $U_m^A$ corresponds by [F10] to the $A$-algebra homomorphism $A[x_{\mathrm{\ell }}^{(m)}:\mathrm{\ell }\mathrm{\ne }m]\to K$ sending $x_{\mathrm{\ell }}^{(m)}$ to $c_{\mathrm{\ell }}:=a_{\mathrm{\ell }}\mathrm{/}{a}_m$, and $c_{\mathrm{\ell }}\in R$ for every $\mathrm{\ell }\mathrm{\ne }m$ by step 3.1.

Define $\phi :A[x_{\mathrm{\ell }}^{(m)}:\mathrm{\ell }\mathrm{\ne }m]\to R$ to be the $A$-algebra homomorphism with $\phi (x_{\mathrm{\ell }}^{(m)})=c_{\mathrm{\ell }}$; it exists and is unique with these values and the prescribed restriction to $A$ by the iterated universal property of polynomial rings [F11], and its composite with $A\to A[x^{(m)}]$ is the structure map $A\to R$ encoded by $b$. Let $c:\mathrm{Spec}R\to U_m^A\subseteq {\mathbb{P}}_A^n\subseteq {\mathbb{P}}_S^n$ be the morphism corresponding to $\phi$ under [F10].

The composite $\pi \circ c$ corresponds under [F10] to the ring map $A\to A[x^{(m)}]\to R$, which is the structure map encoded by $b$; hence $\pi \circ c=b$.

The composite $c\circ j:\mathrm{Spec}K\to U_m^A$ corresponds under [F10] to the $A$-algebra map $A[x^{(m)}]\to K$ sending $x_{\mathrm{\ell }}^{(m)}$ to $c_{\mathrm{\ell }}$, and by step 4.1 this is the same map that the restriction of $a$ to $U_m^A$ corresponds to; hence $c\circ j=a$.

Steps 1.2 through 6.2 produce a lift for an arbitrary valuative diagram for $\pi$ over an arbitrary valuation ring. Since $\pi$ is quasi-compact by step 1.1, [F5] shows that $\pi$ is universally closed. By [F12] a separated, finite-type, universally closed morphism is proper; with steps 1.1 and 1.2 this proves that $\pi :{\mathbb{P}}_S^n\to S$ is proper. The Axiom of Choice [F13] enters exactly through [F5]; the construction chose an affine open $V$, one chart among the finitely many, and the index $m$ by a finite induction, so no other selection is made.