[proofplan] It is enough to prove invariance under each adjacent transposition $x_i \leftrightarrow x_{i+1}$. We construct the Bender-Knuth involution on semistandard tableaux. For a fixed adjacent pair $i,i+1$, entries equal to $i$ or $i+1$ that share a column with the other value are paired and left fixed. The remaining free entries in each row form one consecutive block of $i$'s followed by one consecutive block of $i+1$'s. Interchanging the two block lengths row by row preserves semistandardness, gives an involution, and swaps the two weight coordinates. This pairs monomials in the tableau generating function under the adjacent transposition. Finally, adjacent transpositions generate the symmetric group, and the stable specialization follows because tableaux using an entry whose variable is set to zero contribute zero. [/proofplan] [step:Reduce symmetry to adjacent transpositions] Fix $n$ and write \begin{align*} s_\lambda^{(n)}(x_1,\dots,x_n)=\sum_T x^{\operatorname{wt}(T)} \end{align*} for the tableau generating function, where $T$ ranges over semistandard tableaux of shape $\lambda$ with entries in $\{1,\dots,n\}$. Here \begin{align*} \operatorname{wt}(T)=(\alpha_1(T),\dots,\alpha_n(T))\in \mathbb N^n, \end{align*} $\alpha_k(T)$ is the number of entries of $T$ equal to $k$, and \begin{align*} x^{\operatorname{wt}(T)}=x_1^{\alpha_1(T)}\cdots x_n^{\alpha_n(T)}. \end{align*} Let $S_n$ denote the symmetric group on the set $\{1,\dots,n\}$. The group $S_n$ is generated by the adjacent transpositions $(i,i+1)$ for $1\leq i<n$: any permutation can be sorted to the identity by repeatedly swapping adjacent inversions. Therefore it is enough to prove that $s_\lambda^{(n)}$ is unchanged after interchanging $x_i$ and $x_{i+1}$ for each fixed $i$. [/step] [step:Define paired and free entries] Fix $i$ with $1\leq i<n$. Let $T$ be a semistandard Young tableau. In any column, because entries strictly increase downward, there is at most one entry equal to $i$ and at most one entry equal to $i+1$. If a column contains both values, pair those two boxes and leave them fixed. Call every other box whose entry is $i$ or $i+1$ free. We record the key row structure. In a fixed row, the free entries equal to $i$ or $i+1$ occur as a consecutive string of $i$'s followed by a consecutive string of $i+1$'s, after deleting boxes whose entries are not in $\{i,i+1\}$ and deleting paired boxes. Indeed, rows are weakly increasing, so all entries equal to $i$ occur before all entries equal to $i+1$. Pairing can only remove some of these entries; it cannot create an $i+1$ before a remaining free $i$. Thus the free entries in that row have the displayed form. [/step] [step:Construct the Bender-Knuth move] Let $\mathcal T_\lambda^{(n)}$ be the set of semistandard Young tableaux of shape $\lambda$ with entries in $\{1,\dots,n\}$. We define a map \begin{align*} \tau_i:\mathcal T_\lambda^{(n)}\to \mathcal T_\lambda^{(n)}. \end{align*} For each row $r$, suppose the free entries in that row consist of $a_r$ copies of $i$ followed by $b_r$ copies of $i+1$. Define $\tau_i(T)$ by leaving all entries outside $\{i,i+1\}$ fixed, leaving all paired entries fixed, and replacing the free block in row $r$ by $b_r$ copies of $i$ followed by $a_r$ copies of $i+1$. Rows remain weakly increasing because each altered row still has all $i$'s before all $i+1$'s, and all entries less than $i$ were already to the left of the block while all entries greater than $i+1$ were already to the right. We now check columns. Only columns containing a changed free entry need attention. If a changed entry is $i$, then the entry above it is either absent or at most $i-1$: if the entry above were $i$, then the original entry in this box would have been at least $i+1$ and the two boxes would form a paired column or violate strictness. The entry below a changed $i$ is greater than $i$ because the original tableau was column-strict and changing $i+1$ to $i$ only lowers the entry. If a changed entry is $i+1$, then the entry below it is either absent or at least $i+2$: if the entry below were $i+1$, then the original entry in this box would have been at most $i$ and again the two boxes would form a paired column or violate strictness. The entry above a changed $i+1$ is less than $i+1$ because the original tableau was column-strict and changing $i$ to $i+1$ only raises the entry. Thus $\tau_i(T)$ is semistandard. Applying the same construction again swaps $a_r$ and $b_r$ back in every row and leaves the same paired columns fixed, so $\tau_i$ is an involution. [/step] [step:Show that the move swaps the two weight coordinates] The paired entries consist of one $i$ and one $i+1$ in the same column, so they contribute equally to the two relevant weight coordinates before and after the move. In row $r$, the free contribution changes from $a_r$ entries equal to $i$ and $b_r$ entries equal to $i+1$ to $b_r$ entries equal to $i$ and $a_r$ entries equal to $i+1$. Therefore \begin{align*} \operatorname{wt}(\tau_i(T))_i &= \operatorname{wt}(T)_{i+1},\\ \operatorname{wt}(\tau_i(T))_{i+1} &= \operatorname{wt}(T)_i, \end{align*} and all other weight coordinates are unchanged. [guided] The only entries whose values may change are the free entries equal to $i$ or $i+1$. A paired column contains one $i$ and one $i+1$, and both of those paired entries are fixed, so paired columns make the same contribution to the $i$th and $(i+1)$st weight coordinates before and after applying $\tau_i$. Now look at a single row $r$. Before the move, the free part of that row has $a_r$ entries equal to $i$ and $b_r$ entries equal to $i+1$. After the move, that same free part has $b_r$ entries equal to $i$ and $a_r$ entries equal to $i+1$. Summing over all rows swaps the total number of free $i$'s with the total number of free $i+1$'s, while the paired entries contribute equally on both sides. Hence \begin{align*} \operatorname{wt}(\tau_i(T))_i &= \operatorname{wt}(T)_{i+1},\\ \operatorname{wt}(\tau_i(T))_{i+1} &= \operatorname{wt}(T)_i. \end{align*} Every entry different from $i$ and $i+1$ is fixed, so every other weight coordinate is unchanged. [/guided] [/step] [step:Conclude finite symmetry and stable compatibility] Since $\tau_i$ is a weight-swapping involution on the set of semistandard tableaux of shape $\lambda$ with entries in $\{1,\dots,n\}$, the monomials in \begin{align*} s_\lambda^{(n)}(x_1,\dots,x_n) \end{align*} are paired exactly with the monomials obtained by interchanging $x_i$ and $x_{i+1}$. Hence $s_\lambda^{(n)}$ is invariant under that adjacent transposition. By the first step, $s_\lambda^{(n)}$ is symmetric in $x_1,\dots,x_n$. Finally, recall that $\operatorname{Sym}$ is the stable symmetric-function ring: an element may be represented by a compatible family of symmetric polynomials under the specialization maps that set the newest variable equal to zero. We have \begin{align*} s_\lambda^{(n+1)}(x_1,\dots,x_n,0)=s_\lambda^{(n)}(x_1,\dots,x_n), \end{align*} because every tableau containing the entry $n+1$ contributes a monomial divisible by $x_{n+1}$ and hence vanishes after the specialization, while the remaining tableaux are exactly the tableaux with entries in $\{1,\dots,n\}$. Iterating this one-step identity gives compatibility under the specialization $x_{n+1}=x_{n+2}=\cdots=0$. Thus the compatible finite symmetric polynomials define a stable symmetric function $s_\lambda \in \operatorname{Sym}$. [/step]