Let us define the $n$-permutohedron $P_n$ as the set of all $x\in\mathbb{Q}^n$ such that
$$\sum_{i=1}^n x_i = \binom{n{+}1}{2}\ \ \ \land\ \ \ \forall\,\text{nonempty}\ S\subsetneq\mathbb{N}_n\colon\ \sum_{i\in S} x_i \le \binom{n{+}1}{2} - \binom{n+1-\lvert S\rvert}{2}.$$
I'd like to determine the set of vertices of $P_n$. (Hereby, a vertex of a polyhedron is a point $x$ such that $\{x\}$ is a face). The set of vertices is supposed to be
$$\left\{\left(\sigma(i)\right)_{i=1}^n\,\middle|\, \sigma:\mathbb{N}_n\to\mathbb{N}_n\ \text{is a permutation}\right\},$$
but I'm missing the proof that this set is actually the set of vertices from the aforementioned definition of $P_n$. What would be the easiest low-level, step-by-step, Bourbaki-like way to do this proof? I failed to find a derivation online. Literature references are very welcome.
Let us define $f_S(x)$ to be the value $\sum_{i\in S}x_i$ and $P_S$ to be the plane where $$\sum_{i\in S}x_i={n+1 \choose 2}-{n+1-|S|\choose 2}.$$ We can note that the vertices of the figure can be described exactly as follows:
This is a fairly standard lemma, holding true for any polytope defined by a system of linear equalities and inequalities.
From there, let us consider the intersections of these planes. First, let us prove a lemma: Suppose that $S$ and $S'$ are subsets of $\mathbb N_n$. Let us consider when $P_S\cap P_{S'}$ can intersect the permutohedron. To do this, let $A=S\cap S'$ and $B=S\cup S'$. Note that we have, for any $x$, that: $$f_S(x)+f_{S'}(x)=f_A(x)+f_B(x)$$ For any $x\in P_S\cap P_{S'}$, we can rewrite the lefthand side as follows: $$2{n+1\choose 2}-{n+1-|S|\choose 2}-{n+1-|S'|\choose 2}=f_A(x)+f_B(x)$$ Then, from our constraints, we bound $f_A(x)+f_B(x)$ for any $x$ in the permutohedron: $$f_A(x)+f_B(x)\leq 2{n+1\choose 2}-{n+1-|A|\choose 2}-{n+1-|B|\choose 2}.$$ Composing our two equations gives that, for any $x$ in both $P_S$ and $P_{S'}$ and the permutohedron, we must have: $$2{n+1\choose 2}-{n+1-|S|\choose 2}-{n+1-|S'|\choose 2}\leq 2{n+1\choose 2}-{n+1-|A|\choose 2}-{n+1-|B|\choose 2}.$$ Knowing that $|S|+|S'|=|A|+|B|$ and $|A|\leq \min(|S|,|S'|)$, one can algebraically reduce the above to find that $|A|=\min(|S|,|S'|)$. Since $A$ is their intersection, this implies that $A$ equals either $S$ or $S'$, meaning either $S\subseteq S'$ or $S'\subseteq S$. In particular, unless one of these conditions holds, either $P_S\cap P_S'$ is disjoint from the permutohedron.
Now we are mostly done: if $\mathscr F$ is a family of non-empty subsets of $\mathbb N_n$ and $\bigcap_{S\in F}P_S$ is a single point within the polytope - i.e. it is a vertex - we must have that for any $S,S'\in \mathscr F$ that $S\subseteq S'$ or $S'\subseteq S$. Moreover, since the intersection of fewer than $n$ hyper-planes in $n$ dimensions cannot be a point, we get that $|\mathscr F|\geq n$. In particular, the only families satisfying this are of the form $$\mathscr F = \{\{s_n\},\{s_n,s_{n-1}\},\{s_n,s_{n-1},s_{n-2}\},\ldots,\{s_n,s_{n-1},\ldots,s_1\}\}$$ where $s_i$ is a sequence enumerating $\mathbb N_n$. We can calculate this intersection easily, by letting $\mathscr F_k=\{s_n,s_{n-1},\ldots,s_k\}$ and setting $\mathscr F_{n+1}=\{\}$ for convenience. Then, we have, for any $k$, that $$x_{s_k}=f_{\mathscr F_k}(x)-f_{\mathscr F_{k+1}}(x)=\left({n+1\choose 2}-{k\choose 2}\right)-\left({n+1\choose 2}-{k+1\choose 2}\right)=k$$ Obviously, $x_{s_k}=k$ defines a permutation and can be seen to satisfy all the inequalities defining the permutohedron. Since all possible admissible intersections of the constraint planes give a permutation and all permutations are within the permutohedron, we get that the vertices of the permutohedron are exactly the permutations.