A property implying union-closed sets conjecture condition

Given a union-closed family $$\mathcal{F}$$ of $$n=\vert \mathcal{F} \vert$$ sets, $$n$$ odd, and its family $$\mathit{J}(\mathcal{F})$$ of $$m = \vert\mathit{J}(\mathcal{F})\vert$$ basis sets (or $$\cup$$-irreducible sets, also called generators), and defined $$\mathcal{F_a} = \{A \in \mathcal{F}: a \in A \}$$, the union-closed sets conjecture states that there exists at least one element $$a \in U(\mathcal{F})$$ such that $$\vert \mathcal{F_a} \vert \ge \frac{n}{2}$$.

We furtherly define $$\mathit{J_a}(\mathcal{F}) = \{A \in \mathit{J}(\mathcal{F}) : a \in A \}$$.

I am kindly asking for a verification of the below proof of the following:

Statement

If $$\exists a$$ such that $$\vert\mathit{J_a}(\mathcal{F})\vert \ge m-\Bigl\lfloor\log_2{\frac{n+1}{2}}\Bigr\rfloor$$, then $$\vert \mathcal{F_a} \vert \ge \frac{n}{2}$$.

Proof

With $$k = \frac{n+1}{2}$$, $$A_i \in \mathcal{F}, i = 1 \ldots n$$:

$$\bigcup_{1 \le i_1 \lt \ldots \lt i_k \le n} A_{i_1} \cap \ldots \cap A_{i_k} = \bigcap_{1 \le i_1 \lt \ldots \lt i_k \le n} A_{i_1} \cup \ldots \cup A_{i_k} \tag{1}\label{1}$$

This is because the LHS contains all elements that are in at least $$k$$ of the $$A_i$$ and the RHS contains all elements that are in at least $$n-k+1$$ of the $$A_i$$ (because for each element that does not belong to the RHS we can find $$k$$ $$A_i$$ that do not contain it and thus it is in maximum $$n-k$$ of the $$A_i$$) and note that in our case $$k=n-k+1$$ (see also the answer to this related question).

If we define $$J_i \in J(\mathcal{F}), i = 1 \ldots m$$, then, since the family is union-closed, each union term on the RHS can be expressed as the union of at least $$\lfloor\log_2{k}\rfloor + 1$$ of them. This implies that:

$$\bigcap_{1 \le i_1 \lt \ldots \lt i_{\lfloor\log_2{k}\rfloor + 1}\le m} J_{i_1} \cup \ldots \cup J_{i_{\lfloor\log_2{k}\rfloor + 1}} \subseteq \bigcap_{1 \le i_1 \lt \ldots \lt i_k \le n} A_{i_1} \cup \ldots \cup A_{i_k} \tag{2}\label{2}$$

(we can compute the intersection of the RHS and the LHS and see that it is equal to the LHS). Now the LHS is the set of all $$a \in U(\mathcal{F})$$ such that $$\vert\mathit{J_a}(\mathcal{F})\vert \ge m-\lfloor\log_2{k}\rfloor-1+1 = m-\lfloor\log_2{k}\rfloor$$, for the same argument applied to \eqref{1} above, and thus if it is not empty the RHS will be not empty too.

Is this correct? And explained clearly? Thank you.