A corollary from Sperner's Theorem How can I conclude this fact:
If  $\mathcal{F}$ is an antichain consisting of sets of size at most $k \leq  n/2$, then $|\mathcal{F}|\leq {n\choose k}$
from the Sperner's Theorem:
Let $\mathcal{F}$ be a family of subsets of an $n$ element set. If $\mathcal{F}$ is an antichain, then $|\mathcal{F}|\leq {n\choose \lfloor n/2 \rfloor }$.
 A: Let $[n]=\{1,\dots,n\}$, and let $\binom{[n]}{k}$ denote the set of subsets of $[n]$ with size $k$.
One way to prove Sperner's theorem is to find a sequence of order matchings $f_k$. When $2k<n$, this means that $f_k$ is a injective function $\binom{[n]}{k}\to \binom{[n]}{k+1}$ which satisfies $A\subset f_k(A)$ for all $A\in \binom{[n]}{k}$. When $2k>n$, the mappings go in reverse; $f_k:\binom {[n]}{k}\to \binom{[n]}{k-1}$, but we still require $f_k$ to be injective and satisfy $A\subset f_k(A)$.  These order matchings can be found using Hall's marriage theorem, or using a linear algebra argument (see Stanley, Algebraic Combinatorics, Lemmas 4.5 - 4.7, https://klein.mit.edu/~rstan/algcomb/index.html).
The existence of these mappings for all $k\in \{0,\dots,n\}\setminus \{n/2\}$ implies Sperner's lemma. Namely, given an antichain $\mathcal F$, you can repeatedly apply these order matchings to the sets in $\mathcal F$ to transport them to the middle level of $2^{[n]}$, getting a new antichain $\mathcal F'$ which lives entirely in $\binom{[n]}{\lfloor n/2\rfloor}$. The properties of the order matchings imply $|\mathcal F|=|\mathcal F'|$, so we must have $|\mathcal F|\le \binom{n}{n/2}$.
This same idea easily applies to proving $|\mathcal F|\le \binom{n}{k}$ when all subsets in $\mathcal F$ have size at most $k$, where $k<n/2$. This time, you use the  order matchings to transport each set in $\mathcal F$ to level $k$, and conclude using the same logic.
