Fibre dimension of proper flat finitely presented families

Properness makes every fibre a finite-type scheme over its residue field, hence quasi-compact and of finite Krull dimension when nonempty. Thus the function in the Statement takes only values in $\{-\mathrm{\infty }\}\cup \mathbb{N}$. For every $m\ge 0$ its level set is $\{s:\dim X_s=m\}=L_m\cap (S\setminus C_{m+1})\mathrm{.}$ The first set is open by [F1]; the second is open by [F2]. Therefore every finite-valued level set is open.

The nonempty-fibre locus is exactly $f(X)$. It is open by [F3], because $f$ is flat and locally finitely presented, and closed by [F3], because $f$ is proper. Hence its complement $S\setminus f(X)$, which is precisely the level set with value $-\mathrm{\infty }$, is open and closed.

Every point of $S$ belongs to the open level set of its value by steps 1.1 and 1.2, so the fibre-dimension function is locally constant. If $X=\mathrm{\varnothing }$, the whole base is the $-\mathrm{\infty }$ level set. The dimension zero case uses $L_0\cap (S\setminus C_1)$, and no connectedness or surjectivity hypothesis is needed. AC is inherited through [F1] and [F2]; the set operations use no further choice.