Etale morphisms are universally open and quasi-finite at every point

Flatness, finite presentation and universal openness. Since $f$ is 'etale it is smooth of relative dimension $0$ at every point, hence flat and locally of finite presentation at every point by [F1], i.e. $f$ is flat and locally of finite presentation. By [F2] (AC) $f$ is universally open, so claim 1 holds.

Local quasi-finiteness at a point. Let $x\in X$ and $s=f(x)$. By [F1] $f$ is locally of finite presentation at $x$; by [F3] (AC) in the forward direction, applied at $x$, the morphism is unramified at $x$, so ${\mathrm{\Omega }}_{X\mathrm{/}S,x}=0$. By [F4] the extension $\kappa (x)\mathrm{/}\kappa (s)$ is finite separable and ${\mathfrak{m}}_s{\mathcal{O}}_{X,x}={\mathfrak{m}}_x$. Choose a finite type affine chart $U=\mathrm{Spec}B$ of $x$ over $V=\mathrm{Spec}A\ni s$ with $f(U)\subseteq V$, with $\mathfrak{q}$ the prime of $x$ and $\mathfrak{p}=\mathfrak{q}\cap A$; the fibre algebra is $B_{\mathfrak{q}}\mathrm{/}\mathfrak{p}{B}_{\mathfrak{q}}={\mathcal{O}}_{X,x}\mathrm{/}{\mathfrak{m}}_s{\mathcal{O}}_{X,x}={\mathcal{O}}_{X,x}\mathrm{/}{\mathfrak{m}}_x=\kappa (x)$ by [F5], a finite-dimensional $\kappa (\mathfrak{p})$-vector space because $\kappa (x)\mathrm{/}\kappa (s)$ is finite and $\kappa (\mathfrak{p})=\kappa (s)$ for the affine chart. Hence $f$ is quasi-finite at $x$ in the pointwise sense of [F5].

Global consequence under quasi-compactness. Assume in addition that $f$ is quasi-compact. Since $f$ is locally of finite presentation by [F1], it is locally of finite type, so by [F5] $f$ is of finite type. By step 1.2 the pointwise quasi-finiteness condition holds at every point of $X$, so $f$ is quasi-finite by [F5]. Claim 2 is step 1.2 and claim 3 is this step; the local statement 2 does not require quasi-compactness, which is exactly what the finite type hypothesis of the global notion adds.

Boundary and choice accounting. If $X$ is empty then every pointwise condition is vacuous and claims 1, 2 and 3 hold vacuously, including the empty source case of quasi-finiteness recorded in [F5]; the Axiom of Choice [F6] is assumed in the Statement and used exactly through [F2] in step 1.1 and through [F3] and [F4] in step 1.2, while steps 2.1 and this step add no choice. [F2, F3, F4, F5, F6, step 1.1, step 1.2, step 2.1] $\mathrm{\square }$