[proofplan]
We prove that the two displayed maps are well-defined and inverse to each other. First, maximal elements of an order ideal form an antichain, and finiteness ensures that every element of the ideal lies below some maximal element. Conversely, the down-set generated by an antichain is an order ideal, and its maximal elements are exactly the original antichain.
[/proofplan]
[step:Show that maximal elements of an order ideal form an antichain]
Let $I\in \mathcal J(P)$ be an order ideal. If $u,v\in \max(I)$ and $u\le v$, then maximality of $u$ in $I$ gives $u=v$. Therefore no two distinct elements of $\max(I)$ are comparable, so $\max(I)$ is an antichain. Thus $\Phi$ is well-defined.
[/step]
[step:Recover an order ideal from its maximal elements]
Let $I\in \mathcal J(P)$. We prove
\begin{align*}
I=\langle \max(I)\rangle.
\end{align*}
First, if $x\in \langle \max(I)\rangle$, then there exists $m\in \max(I)$ such that $x\le m$. Since $m\in I$ and $I$ is an order ideal, downward closure gives $x\in I$. Hence
\begin{align*}
\langle \max(I)\rangle\subset I.
\end{align*}
Conversely, let $x\in I$. Consider the finite subset
\begin{align*}
I_{\ge x}:=\{y\in I:x\le y\}.
\end{align*}
This set is nonempty because $x\in I_{\ge x}$. Since $I_{\ge x}$ is finite, it has an element $m$ such that no element of $I_{\ge x}$ is strictly larger than $m$. We claim that $m\in \max(I)$. Indeed, if $m\le z$ for some $z\in I$, then $x\le m\le z$, so $z\in I_{\ge x}$; by the choice of $m$, this forces $z=m$. Thus $m$ is maximal in $I$. Since $x\le m$, we have $x\in \langle \max(I)\rangle$. Therefore
\begin{align*}
I\subset \langle \max(I)\rangle.
\end{align*}
The two inclusions prove $I=\langle \max(I)\rangle$.
[guided]
The point of this step is to identify exactly where finiteness is used. Let $I\in \mathcal J(P)$. We want to prove
\begin{align*}
I=\langle \max(I)\rangle.
\end{align*}
We first prove the inclusion from right to left. Suppose $x\in \langle \max(I)\rangle$. By definition of the generated down-set, there exists $m\in \max(I)$ such that $x\le m$. Since $m\in I$ and $I$ is an order ideal, every element below $m$ must also belong to $I$. Hence $x\in I$, and therefore
\begin{align*}
\langle \max(I)\rangle\subset I.
\end{align*}
For the reverse inclusion, fix $x\in I$. We need to find a maximal element of $I$ above $x$. Define
\begin{align*}
I_{\ge x}:=\{y\in I:x\le y\}.
\end{align*}
This is a finite nonempty subset of $P$: it is finite because $P$ is finite, and it is nonempty because $x\in I_{\ge x}$. Since $I_{\ge x}$ is finite, we may choose an element $m\in I_{\ge x}$ such that there is no element of $I_{\ge x}$ strictly above $m$.
We now verify that this $m$ is maximal in $I$, not merely maximal among elements above $x$. Let $z\in I$ satisfy $m\le z$. Because $x\le m$ and $m\le z$, transitivity gives $x\le z$. Hence $z\in I_{\ge x}$. The choice of $m$ as a maximal element of $I_{\ge x}$ then implies $z=m$. Thus no element of $I$ is strictly above $m$, so $m\in \max(I)$.
Finally, since $x\le m$ and $m\in \max(I)$, the definition of $\langle \max(I)\rangle$ gives $x\in \langle \max(I)\rangle$. Since $x\in I$ was arbitrary, we have
\begin{align*}
I\subset \langle \max(I)\rangle.
\end{align*}
Combining the two inclusions gives
\begin{align*}
I=\langle \max(I)\rangle.
\end{align*}
[/guided]
[/step]
[step:Show that the down-set generated by an antichain is an order ideal]
Let $A\in \mathcal A(P)$ be an antichain, and define
\begin{align*}
\langle A\rangle=\{x\in P:x\le a \text{ for some } a\in A\}.
\end{align*}
If $y\in \langle A\rangle$ and $x\le y$, then there exists $a\in A$ such that $y\le a$. By transitivity, $x\le a$, so $x\in \langle A\rangle$. Hence $\langle A\rangle$ is an order ideal, and $\Psi$ is well-defined.
[/step]
[step:Recover an antichain from its generated order ideal]
Let $A\in \mathcal A(P)$. We prove
\begin{align*}
\max(\langle A\rangle)=A.
\end{align*}
First let $a\in A$. Since $a\le a$, we have $a\in \langle A\rangle$. Suppose $a\le y$ for some $y\in \langle A\rangle$. By definition of $\langle A\rangle$, there exists $b\in A$ such that $y\le b$. Thus
\begin{align*}
a\le y\le b.
\end{align*}
Because $A$ is an antichain and $a,b\in A$, the comparability $a\le b$ forces $a=b$. Then $a\le y\le a$, so antisymmetry gives $y=a$. Hence $a$ is maximal in $\langle A\rangle$, and so
\begin{align*}
A\subset \max(\langle A\rangle).
\end{align*}
Conversely, let $x\in \max(\langle A\rangle)$. Since $x\in \langle A\rangle$, there exists $a\in A$ such that $x\le a$. Also $a\in \langle A\rangle$ because $a\le a$. Maximality of $x$ in $\langle A\rangle$ therefore implies $x=a$. Hence $x\in A$, and
\begin{align*}
\max(\langle A\rangle)\subset A.
\end{align*}
Thus $\max(\langle A\rangle)=A$.
[/step]
[step:Conclude that the two constructions are inverse bijections]
The equality
\begin{align*}
I=\langle \max(I)\rangle
\end{align*}
for every $I\in \mathcal J(P)$ says that
\begin{align*}
\Psi(\Phi(I))=I.
\end{align*}
The equality
\begin{align*}
\max(\langle A\rangle)=A
\end{align*}
for every $A\in \mathcal A(P)$ says that
\begin{align*}
\Phi(\Psi(A))=A.
\end{align*}
Therefore $\Phi$ and $\Psi$ are inverse maps. Hence $\Phi:I\mapsto \max(I)$ is a bijection from order ideals of $P$ to antichains of $P$, with inverse $A\mapsto \langle A\rangle$.
[/step]
