Antichain trace bound for intersection-free families ($|\mathcal{F}|\le 1+\left(\genfrac{}{}{0ex}{}{r}{\lfloor r/2\rfloor }\right)$)

For an intersection-free uniform set family of rank $r$, fix $X\in \mathcal{F}$. The map $A\mapsto X\cap A$ on $\mathcal{F}\setminus \{X\}$ is injective and its image is an antichain in $\mathcal{P}(X)$: a containment $X\cap A\subseteq X\cap B$ would violate intersection-freeness on the distinct members $X,A,B$. The Sperner theorem then proves the displayed bound.