[proofplan]
We compare the normalized LYM sum of an arbitrary antichain with its ordinary cardinality. Let $M$ be the largest rank level size. Since every element of an antichain lies in a rank level of size at most $M$, each LYM summand is at least $1/M$. The assumed [LYM inequality](/theorems/2586) then forces every antichain to have size at most $M$, while a rank level of size $M$ is itself an antichain, so the bound is attained.
[/proofplan]
[step:Choose a largest rank level]
Define
\begin{align*}
M=\max_{0\le i\le r}|P_i|.
\end{align*}
Since $P$ has rank levels $P_0,\dots,P_r$, the set over which the maximum is taken is finite. Since $P$ is nonempty, at least one rank level is nonempty, so $M$ is a positive integer. Choose an index $i_0\in\{0,\dots,r\}$ such that
\begin{align*}
|P_{i_0}|=M.
\end{align*}
[/step]
[step:Bound the size of an arbitrary antichain by the largest rank level]
Let $A\subset P$ be an antichain. For each $x\in A$, the element $x$ belongs to the rank level $P_{\rho(x)}$, and by the definition of $M$ we have
\begin{align*}
|P_{\rho(x)}|\le M.
\end{align*}
Since $|P_{\rho(x)}|$ and $M$ are positive integers for every $x\in A$, taking reciprocals reverses the inequality:
\begin{align*}
\frac{1}{|P_{\rho(x)}|}\ge \frac{1}{M}.
\end{align*}
Summing this inequality over all $x\in A$ gives
\begin{align*}
\sum_{x\in A}\frac{1}{|P_{\rho(x)}|}\ge \sum_{x\in A}\frac{1}{M}.
\end{align*}
The right-hand side is
\begin{align*}
\sum_{x\in A}\frac{1}{M}=\frac{|A|}{M}.
\end{align*}
By the assumed LYM inequality applied to the antichain $A$,
\begin{align*}
\sum_{x\in A}\frac{1}{|P_{\rho(x)}|}\le 1.
\end{align*}
Combining the two inequalities yields
\begin{align*}
\frac{|A|}{M}\le 1.
\end{align*}
Multiplying by the positive integer $M$ gives
\begin{align*}
|A|\le M.
\end{align*}
[guided]
The purpose of the LYM inequality is to control a weighted count of an antichain. We want to turn that weighted count into an ordinary count. Let $A\subset P$ be an arbitrary antichain. For every element $x\in A$, the rank $\rho(x)$ is defined because $P$ is ranked, so $x$ lies in the rank level $P_{\rho(x)}$.
By definition,
\begin{align*}
M=\max_{0\le i\le r}|P_i|.
\end{align*}
Therefore every rank level has size at most $M$, and in particular
\begin{align*}
|P_{\rho(x)}|\le M
\end{align*}
for each $x\in A$. Since $x\in P_{\rho(x)}$, the denominator $|P_{\rho(x)}|$ is a positive integer. Also $M$ is positive because it is at least $|P_{\rho(x)}|$ for any $x\in A$; if $A=\varnothing$, then the desired inequality $|A|\le M$ is immediate. Thus, for nonempty $A$, taking reciprocals gives
\begin{align*}
\frac{1}{|P_{\rho(x)}|}\ge \frac{1}{M}.
\end{align*}
Now sum this pointwise inequality over the finite set $A$:
\begin{align*}
\sum_{x\in A}\frac{1}{|P_{\rho(x)}|}\ge \sum_{x\in A}\frac{1}{M}.
\end{align*}
The summand $1/M$ is constant in $x$, so the right-hand side is exactly
\begin{align*}
\sum_{x\in A}\frac{1}{M}=\frac{|A|}{M}.
\end{align*}
The hypothesis says that every antichain satisfies the LYM inequality. Since $A$ is an antichain, we may apply that hypothesis to obtain
\begin{align*}
\sum_{x\in A}\frac{1}{|P_{\rho(x)}|}\le 1.
\end{align*}
Putting the lower bound and upper bound together gives
\begin{align*}
\frac{|A|}{M}\le 1.
\end{align*}
Multiplication by the positive integer $M$ preserves the inequality, hence
\begin{align*}
|A|\le M.
\end{align*}
Because $A$ was arbitrary, no antichain in $P$ has more than $M$ elements.
[/guided]
[/step]
[step:Show that the upper bound is attained by a rank level]
We verify that the rank level $P_{i_0}$ is an antichain. If $x,y\in P_{i_0}$ and $x<y$, then the defining property of the rank function gives
\begin{align*}
\rho(x)<\rho(y).
\end{align*}
But $\rho(x)=i_0=\rho(y)$, a contradiction. Hence no two distinct elements of $P_{i_0}$ are comparable, so $P_{i_0}$ is an antichain.
From the previous step, every antichain has size at most $M$. Since $P_{i_0}$ is an antichain and $|P_{i_0}|=M$, the maximum size of an antichain is exactly
\begin{align*}
M=\max_{0\le i\le r}|P_i|.
\end{align*}
Therefore $P$ is Sperner.
[/step]
