[proofplan] We first verify that $\Phi(x)$ is an order ideal of the join-irreducible poset $P$. The central finite-lattice ingredient is that every element of $L$ is the join of the join-irreducible elements below it; this is proved by a minimal-counterexample argument using the definition of join-irreducibility. Distributivity then upgrades join-irreducibility to join-primality, which is the key point in proving surjectivity onto all order ideals. Finally, the order bijection is shown directly to preserve meet and join. [/proofplan] [step:Show that $\Phi$ is a well-defined order-preserving map into $J(P)$] Let $x\in L$. We prove that $\Phi(x)$ is an order ideal of $P$. Suppose $j\in \Phi(x)$ and $k\in P$ satisfy $k\le j$ in $P$. Since the order on $P$ is inherited from $L$, we have $k\le j\le x$ in $L$, so $k\in \Phi(x)$. Hence $\Phi(x)$ is downward closed in $P$, and therefore $\Phi(x)\in J(P)$. If $x,y\in L$ and $x\le y$, then every $j\in P$ with $j\le x$ also satisfies $j\le y$. Thus \begin{align*} \Phi(x)\subseteq \Phi(y). \end{align*} So $\Phi:L\to J(P)$ is well-defined and order-preserving. [/step] [step:Decompose every lattice element as the join of the join-irreducibles below it] For a finite subset $S\subset L$, write $\bigvee S$ for its join, with the convention that $\bigvee \varnothing=\hat{0}$. [claim:Every element is generated by the join-irreducibles below it] For every $x\in L$, \begin{align*} x=\bigvee \Phi(x). \end{align*} [/claim] [proof] Assume, for contradiction, that the claim fails. Since $L$ is finite, the set of counterexamples has a minimal element with respect to the lattice order; call it $x_0\in L$. The element $x_0$ cannot be $\hat{0}$, because $\Phi(\hat{0})=\varnothing$ under the convention that join-irreducible elements are not equal to $\hat{0}$, and therefore \begin{align*} \bigvee \Phi(\hat{0})=\bigvee \varnothing=\hat{0}. \end{align*} If $x_0\in P$, then $x_0\in \Phi(x_0)$, and hence \begin{align*} x_0\le \bigvee \Phi(x_0)\le x_0. \end{align*} Thus $x_0=\bigvee \Phi(x_0)$, contradicting that $x_0$ is a counterexample. Therefore $x_0\notin P$ and $x_0\ne \hat{0}$. By the definition of join-irreducibility, there exist $a,b\in L$ such that \begin{align*} x_0=a\vee b \end{align*} with $a\ne x_0$ and $b\ne x_0$. Since $a\le a\vee b=x_0$ and $b\le a\vee b=x_0$, this gives $a<x_0$ and $b<x_0$. By minimality of $x_0$, neither $a$ nor $b$ is a counterexample, so \begin{align*} a=\bigvee \Phi(a) \end{align*} and \begin{align*} b=\bigvee \Phi(b). \end{align*} Since $\Phi(a)\subseteq \Phi(x_0)$ and $\Phi(b)\subseteq \Phi(x_0)$, we obtain \begin{align*} x_0=a\vee b=\left(\bigvee \Phi(a)\right)\vee\left(\bigvee \Phi(b)\right)\le \bigvee \Phi(x_0). \end{align*} The reverse inequality $\bigvee \Phi(x_0)\le x_0$ holds because every element of $\Phi(x_0)$ is below $x_0$. Hence $x_0=\bigvee \Phi(x_0)$, again a contradiction. This proves the claim. [/proof] [guided] The point of this step is to show that no element of the finite distributive lattice is invisible to the join-irreducibles. For a finite subset $S\subset L$, we write $\bigvee S$ for the join of all elements of $S$, and we use the convention \begin{align*} \bigvee \varnothing=\hat{0}. \end{align*} We prove that every $x\in L$ satisfies \begin{align*} x=\bigvee \Phi(x). \end{align*} Suppose this is false. Because $L$ is finite, there is a minimal counterexample $x_0\in L$. The bottom element cannot be a counterexample: since join-irreducible elements are defined to exclude $\hat{0}$, no element of $P$ lies below $\hat{0}$ except possibly $\hat{0}$ itself, which is not in $P$. Thus $\Phi(\hat{0})=\varnothing$, and the empty-join convention gives \begin{align*} \bigvee \Phi(\hat{0})=\hat{0}. \end{align*} Next suppose $x_0$ itself is join-irreducible. Then $x_0\in P$ and $x_0\le x_0$, so $x_0\in \Phi(x_0)$. Since every element of $\Phi(x_0)$ is also below $x_0$, we have both inequalities \begin{align*} x_0\le \bigvee \Phi(x_0) \end{align*} and \begin{align*} \bigvee \Phi(x_0)\le x_0. \end{align*} Therefore $x_0=\bigvee \Phi(x_0)$, contradicting the choice of $x_0$. So $x_0$ is neither $\hat{0}$ nor join-irreducible. By the definition of join-irreducibility, there are $a,b\in L$ such that \begin{align*} x_0=a\vee b \end{align*} and neither $a$ nor $b$ equals $x_0$. Since each of $a$ and $b$ is below their join $x_0$, this means \begin{align*} a<x_0 \end{align*} and \begin{align*} b<x_0. \end{align*} Minimality of $x_0$ now applies to both $a$ and $b$, giving \begin{align*} a=\bigvee \Phi(a) \end{align*} and \begin{align*} b=\bigvee \Phi(b). \end{align*} Because $a\le x_0$ and $b\le x_0$, order-preservation from the previous step gives \begin{align*} \Phi(a)\subseteq \Phi(x_0) \end{align*} and \begin{align*} \Phi(b)\subseteq \Phi(x_0). \end{align*} Thus \begin{align*} x_0=a\vee b=\left(\bigvee \Phi(a)\right)\vee\left(\bigvee \Phi(b)\right)\le \bigvee \Phi(x_0). \end{align*} The opposite inequality holds because every element being joined in $\Phi(x_0)$ is, by definition, at most $x_0$. Hence \begin{align*} x_0=\bigvee \Phi(x_0), \end{align*} contradicting that $x_0$ was a counterexample. This contradiction proves the decomposition for every element of $L$. [/guided] [/step] [step:Prove that $\Phi$ is injective by reconstructing each element from its image] Let $x,y\in L$ and suppose $\Phi(x)=\Phi(y)$. By the decomposition just proved, \begin{align*} x=\bigvee \Phi(x) \end{align*} and \begin{align*} y=\bigvee \Phi(y). \end{align*} Since the two indexing sets are equal, the two joins are equal. Hence $x=y$, so $\Phi$ is injective. [/step] [step:Use distributivity to prove join-irreducibles are join-prime] We record the finite form of join-primality needed for surjectivity. Let $j\in P$ and let $S\subset L$ be finite. If \begin{align*} j\le \bigvee S, \end{align*} then there exists $s\in S$ such that $j\le s$. It is enough to prove the binary case, because the finite case then follows by induction on $|S|$, with the empty case impossible since $j\ne \hat{0}$ and $j\le \bigvee \varnothing=\hat{0}$ cannot hold. Suppose $a,b\in L$ and $j\le a\vee b$. Using distributivity in $L$, \begin{align*} j=j\wedge(a\vee b)=(j\wedge a)\vee(j\wedge b). \end{align*} Since $j$ is join-irreducible, either \begin{align*} j=j\wedge a \end{align*} or \begin{align*} j=j\wedge b. \end{align*} In the first case $j\le a$, and in the second case $j\le b$. This proves the binary case and hence the finite case. [/step] [step:Construct a preimage for every order ideal] Let $I\in J(P)$ be an order ideal. Define \begin{align*} x_I=\bigvee I\in L, \end{align*} again with the convention $x_I=\hat{0}$ when $I=\varnothing$. We prove that $\Phi(x_I)=I$. If $i\in I$, then $i\le \bigvee I=x_I$, so $i\in \Phi(x_I)$. Hence \begin{align*} I\subseteq \Phi(x_I). \end{align*} Conversely, let $j\in \Phi(x_I)$. Then $j\in P$ and \begin{align*} j\le x_I=\bigvee I. \end{align*} By the join-primality result from the previous step, there exists $i\in I$ such that $j\le i$. Since $I$ is an order ideal in $P$ and $j\in P$, downward closure gives $j\in I$. Therefore \begin{align*} \Phi(x_I)\subseteq I. \end{align*} Thus $\Phi(x_I)=I$. Since $I\in J(P)$ was arbitrary, $\Phi$ is surjective. [/step] [step:Verify that the bijection preserves meet and join] Let $x,y\in L$. For meet, a join-irreducible $j\in P$ satisfies $j\le x\wedge y$ if and only if $j\le x$ and $j\le y$. Hence \begin{align*} \Phi(x\wedge y)=\Phi(x)\cap \Phi(y). \end{align*} For join, first $\Phi(x)\cup\Phi(y)\subseteq \Phi(x\vee y)$ because $x\le x\vee y$ and $y\le x\vee y$. Conversely, if $j\in \Phi(x\vee y)$, then $j\in P$ and \begin{align*} j\le x\vee y. \end{align*} By the binary join-primality proved above, either $j\le x$ or $j\le y$. Hence $j\in \Phi(x)\cup\Phi(y)$. Therefore \begin{align*} \Phi(x\vee y)=\Phi(x)\cup\Phi(y). \end{align*} The meet and join in $J(P)$ are intersection and union, respectively. Thus $\Phi$ preserves both lattice operations. Since $\Phi$ is also bijective, $\Phi:L\to J(P)$ is a lattice isomorphism. [/step]