co.combinatorics - Maximum size of antichain if no m subsets have a common intersection of size n

I have a lemma about antichains that I think should be already known, but I can't find it anywhere. I am looking for a reference to this result that I can use in my paper, so that I don't have to include the proof.

Let $mathcal{F}$ be an antichain on finite universe $U$, such that there are no $m$ distinct subsets $S_1, S_2, ldots, S_m in mathcal{F}$ such that $|S_1 cap S_2 ldots cap S_m| geq n$. Then $|mathcal{F}| leq 2m|U|^n$.

(The bound can actually be made a little bit sharper, but this is sufficient for my purposes.)

Here is a proof of why this claim is true. We count the number of sets in $mathcal{F}$ in two steps.

1) Since $mathcal{F}$ is an antichain, all sets in it are distinct. Hence there are less than $|U|^k$ sets in $F$ of size $k$. Hence the number of sets in $mathcal{F}$ of size at most $n-1$ is less than $sum _{k=0}^{n-1} |U|^k = (U^n - 1)/(U - 1) leq U^n$.

2) Now we count the number of sets with at least $n$ elements. For each set in $mathcal{F}$ with at least $n$ elements, select $n$ of its elements arbitrarily and group the sets according to the chosen $n$ elements. If some group contains at least $m$ subsets of $mathcal{F}$, then the $n$ elements that define the group are in the common intersection of these $m$ subsets, and this violates our assumption. Hence every group has less than $m$ subsets in it. Since there are less than $|U|^n$ different groups, and each group has less than $m$ subsets in it, there are less than $m|U|^n$ subsets in $mathcal{F}$ of size at least $n$.

Adding the numbers from (1) and (2) yields that the total number of subsets in $mathcal{F}$ is bounded by $2m|U|^n$.

Can anyone tell me if this is already known and under which name? A reference would be greatly appreciated. Thanks!