Involution that brings sets to disjoint sets

Here's a proof which gives an algorithm for constructing an involution. If the order ideal $\mathcal{A}=\emptyset$ we're done; otherwise we can select a maximal element $X$ of $\mathcal{A}$ (with respect to inclusion.) If we're really lucky, there is another maximal element $Y$ of $\mathcal{A}$ disjoint from $X$. If so, we can set $X\leftrightarrow Y$; since $\mathcal{A}'=\mathcal{A}\setminus\{X,Y\}$ is an order ideal, we can find a suitable involution on $\mathcal{A}'$ by induction on $|\mathcal{A}|$, so we're done.

In general, we won't be so lucky, but the intuition is the same. Given a maximal element $X$ of $\mathcal{A}$, select a maximal element $Y$ in $\{ Y\in \mathcal{A}\mid Y\cap X=\emptyset \}.$ We can pair $X$ with $Y$, but in general $Y$ is not maximal in $\mathcal{A}$ so we have to do a little more work before we can appeal to induction. By the choice of $Y$, every set in $\mathcal{A}$ containing $Y$ has the form $Y\cup B$ for some $B\subset X$. Let $$\mathcal{B} =\{B\subset X\mid Y\cup B\in\mathcal{A}\};$$ note that $\mathcal{B}$ is closed under taking subsets since $\mathcal{A}$ is.

For each $B\in\mathcal{B}$, we pair $Y\cup B$ with $X\setminus B$ (which we know is in $\mathcal{A}$ since $\mathcal{A}$ is an order ideal.) In short, this matches the elements of $Y\cup\mathcal{B}$ with the elements of $X\setminus\mathcal{B}$. Let $\mathcal{A}'$ be the result of removing all these paired elements from $\mathcal{A}$. Once we check $\mathcal{A}'$ is an order ideal, we're done by induction.

All we need to check is that the set of elements we removed is an order coideal of $\mathcal{A}$. (i.e. if we removed $Z$, and $W\supset Z$ is in $\mathcal{A}$, then we also removed $W$). But $Y\cup \mathcal{B}$ is an order coideal by construction; $X\setminus\mathcal{B}$ is one since $\mathcal{B}$ is an order ideal; and the union of order coideals is an order coideal. So $\mathcal{A}'$ is an order ideal, and we're done by induction. $\square$

Remark: if $\mathcal{A}$ is the power set of $X$, then $X$ is the unique maximal element of $\mathcal{A}$; the algorithm picks $Y=\emptyset$, and pairs each $B$ with the complement $X\setminus B$, so this generalizes the special case pointed out in the original post. It also generalizes the special case at the beginning of the post: if $Y$ is maximal in $\mathcal{A}$ then $\mathcal{B}=\emptyset.$