[proofplan] We prove bijectivity by constructing an explicit inverse using reverse row insertion. Starting from a pair of standard tableaux $(P,Q)$ of common shape with $n$ boxes, we remove the box containing $n$ in $Q$, reverse the corresponding last insertion in $P$, and thereby recover the last letter $w_n$. Iterating this procedure recovers $w_n,w_{n-1},\dots,w_1$, and the local inverse property of reverse row insertion shows that this reconstruction is inverse to the forward RSK algorithm. [/proofplan]

[step:Fix the row insertion and reverse row insertion conventions]Let $A=\{1,\dots,n\}$ with its usual total order. For a row- and column-increasing tableau $T$ with entries in $A$ and for a letter $a\in A$ not already appearing in $T$, row insertion of $a$ into $T$ is the following algorithm. In the first row, if every entry is smaller than $a$, append $a$ at the end of that row and stop. Otherwise, let $b$ be the leftmost entry larger than $a$, replace $b$ by $a$, and insert $b$ into the next row by the same rule. The process stops when some letter is appended to the end of a row, and the newly created box is called the added box. By [Schensted Insertion Produces A Tableau][citetheorem:8429], successive row insertions of pairwise distinct letters produce a row- and column-increasing tableau filled by those letters. Now define the reverse row insertion operation. Let $T$ be a standard tableau and let $\square$ be a removable corner of its shape. Suppose $\square$ lies in row $r$. Remove the entry in $\square$ from row $r$ and call it $x_r$. For $i=r-1,r-2,\dots,1$, choose $x_i$ to be the rightmost entry in row $i$ that is smaller than $x_{i+1}$, replace that entry by $x_{i+1}$, and continue upward. The final output letter is $x_1$, and the resulting tableau has one fewer box. This reverse operation is defined precisely on the boxes that can arise as added boxes in row insertion. Indeed, during forward row insertion, an entry is bumped from row $i$ exactly when it is the leftmost entry larger than the entering letter; equivalently, when reversing from the next row, that same entry is recovered as the rightmost entry in row $i$ smaller than the letter moving upward. Therefore reverse row insertion undoes one forward row insertion step, row by row, and forward row insertion undoes one reverse row insertion step by the same comparison rule.[/step]

[guided]The point of fixing conventions is that RSK has several equivalent versions, and the inverse depends on the exact bumping rule. Here the forward rule is row insertion with the convention: when a letter enters a row, it bumps the leftmost entry that is larger than it. Let $T$ be a row- and column-increasing tableau and let $a$ be a letter not appearing in $T$. Row insertion sends $a$ into the first row. If no entry is larger than $a$, the algorithm appends $a$ and stops. If there is a larger entry, it chooses the leftmost such entry, bumps it, and repeats the same operation in the next row. Since each bump moves one row downward and a finite tableau has only finitely many occupied rows, the algorithm terminates by adding one new box. The reverse operation starts with a tableau $T$ and a removable corner $\square$. Removing a corner preserves the Young diagram property. If $\square$ is in row $r$, write $x_r$ for the removed entry. Then move upward. In row $i$, choose the rightmost entry smaller than the letter $x_{i+1}$ moving upward, replace that entry by $x_{i+1}$, and call the removed entry $x_i$. After reaching row $1$, the output is $x_1$. Why is this the inverse rule? In the forward algorithm, if an entering letter $a$ bumps an entry $b$ from a row, then $b$ is the leftmost entry in that row satisfying $b>a$. After replacement, the row contains $a$ in the position formerly occupied by $b$. When reversing from the next row, the letter moving upward is $b$, and the entry that must be removed from the previous row is precisely $a$. Because the row is increasing and $b$ originally was the leftmost entry larger than $a$, the entry $a$ is exactly the rightmost entry in the modified row smaller than $b$. Thus the reverse comparison recovers the exact previous entry and the exact previous position. Repeating this row by row proves that one reverse row insertion step undoes one forward row insertion step, and conversely.[/guided]

[step:Show that the forward RSK map lands in pairs of standard tableaux of common shape] Let $w=w_1\cdots w_n\in S_n$. Since $w$ is a permutation of $\{1,\dots,n\}$, the letters $w_1,\dots,w_n$ are pairwise distinct. Define $P_0$ and $Q_0$ to be the empty tableaux. For $1\le k\le n$, define $P_k$ to be the tableau obtained from $P_{k-1}$ by row-inserting $w_k$, and define $Q_k$ by adding to $Q_{k-1}$ the same new box and placing the entry $k$ in that box. By [Schensted Insertion Produces A Tableau][citetheorem:8429], each $P_k$ is row- and column-increasing and has entries $\{w_1,\dots,w_k\}$. Since these entries are distinct, $P_n$ is a standard Young tableau with entries $\{1,\dots,n\}$. It remains to check the recording tableau. At step $k$, the shape changes by adding one removable corner. Thus $Q_k$ is filled by $\{1,\dots,k\}$. Since the entry $k$ is placed in a newly added outer corner, every existing neighbor immediately to its left or above, if present, was already filled by a number in $\{1,\dots,k-1\}$. Hence rows and columns remain increasing. Therefore $Q_n$ is a standard Young tableau. By construction, $P_n$ and $Q_n$ have the same shape. Thus \begin{align*} \operatorname{RSK}_n(w)=(P_n,Q_n)\in \bigsqcup_{\lambda\vdash n}\operatorname{SYT}(\lambda)\times\operatorname{SYT}(\lambda). \end{align*} [/step]

[step:Construct the inverse map by repeatedly removing the largest recording entry] Let $(P,Q)\in \operatorname{SYT}(\lambda)\times \operatorname{SYT}(\lambda)$ for some partition $\lambda\vdash n$. We define a reconstruction procedure. Set $P^{(n)}=P$ and $Q^{(n)}=Q$. For $k=n,n-1,\dots,1$, let $\square_k$ be the box containing $k$ in $Q^{(k)}$. Since $Q^{(k)}$ is standard, no box can lie immediately to the right of $\square_k$ or immediately below $\square_k$; otherwise that neighboring box would contain an entry larger than $k$, impossible because the entries of $Q^{(k)}$ are exactly $\{1,\dots,k\}$. Hence $\square_k$ is a removable corner. Remove $\square_k$ from $Q^{(k)}$ to obtain $Q^{(k-1)}$. Perform reverse row insertion on $P^{(k)}$ starting from the same removable corner $\square_k$. Let $a_k$ be the output letter, and let $P^{(k-1)}$ be the resulting tableau. The local inverse property from the preceding step shows that $P^{(k-1)}$ is standard and has entries equal to the entries of $P^{(k)}$ with $a_k$ removed. Inductively, the entries removed from $P$ are pairwise distinct and exhaust $\{1,\dots,n\}$. Thus the word \begin{align*} a_1a_2\cdots a_n \end{align*} is the one-line notation of an element of $S_n$. Define \begin{align*} \Psi_n:\bigsqcup_{\lambda\vdash n}\operatorname{SYT}(\lambda)\times\operatorname{SYT}(\lambda)&\to S_n \end{align*} \begin{align*} (P,Q)&\mapsto a_1a_2\cdots a_n \end{align*} by this reconstruction algorithm. [/step]

[step:Verify that reconstruction undoes the forward algorithm] Let $w=w_1\cdots w_n\in S_n$, and let \begin{align*} \operatorname{RSK}_n(w)=(P_n,Q_n). \end{align*} In the forward construction, the entry $n$ of $Q_n$ is placed exactly in the box added when inserting $w_n$ into $P_{n-1}$. Therefore the first step of the reconstruction removes that box from $Q_n$ and applies reverse row insertion to the box created by inserting $w_n$. By the local inverse property of reverse row insertion, this recovers the output letter $w_n$ and returns the insertion tableau to $P_{n-1}$. Repeating the same argument for $k=n-1,n-2,\dots,1$ gives recovered letters \begin{align*} a_k=w_k \end{align*} for every $1\le k\le n$. Therefore \begin{align*} \Psi_n(\operatorname{RSK}_n(w))=w. \end{align*} So $\Psi_n\circ \operatorname{RSK}_n$ is the identity map on $S_n$. [/step]

[step:Verify that the forward algorithm undoes reconstruction] Let $(P,Q)\in \operatorname{SYT}(\lambda)\times\operatorname{SYT}(\lambda)$ for some $\lambda\vdash n$, and let \begin{align*} \Psi_n(P,Q)=a_1a_2\cdots a_n. \end{align*} During reconstruction, for each $k$, the pair $(P^{(k)},Q^{(k)})$ is obtained from $(P^{(k-1)},Q^{(k-1)})$ by inserting the recovered letter $a_k$ into $P^{(k-1)}$ and recording the new box with the entry $k$. This is exactly the forward row-insertion step, because reverse row insertion and row insertion are local inverses with the same bumping comparisons. Starting with the empty pair $(P^{(0)},Q^{(0)})$ and inserting $a_1,\dots,a_n$ therefore reconstructs successively \begin{align*} (P^{(1)},Q^{(1)}),\ (P^{(2)},Q^{(2)}),\ \dots,\ (P^{(n)},Q^{(n)})=(P,Q). \end{align*} Hence \begin{align*} \operatorname{RSK}_n(\Psi_n(P,Q))=(P,Q). \end{align*} So $\operatorname{RSK}_n\circ \Psi_n$ is the identity map on the disjoint union of pairs of standard Young tableaux of common shape. The map $\operatorname{RSK}_n$ has a two-sided inverse $\Psi_n$. Therefore $\operatorname{RSK}_n$ is a bijection. [/step]