Birkhoff representation theorem: every finite distributive lattice is isomorphic to the lattice of order ideals of its join-irreducible poset

The poset $P$ is finite because it is a subset of $L$. For every $x\in L$, the set $\mathrm{\Phi }(x)$ is an order ideal of $P$: if $j\le x$ and $i\in P$ satisfies $i\le j$, then $i\le x$. Thus $\mathrm{\Phi }$ is well defined.

For an order ideal $I\in J(P)$, construct $\mathrm{\Psi }(I):=\bigvee I$, taking $\mathrm{\Psi }(\mathrm{\varnothing })=0_L$. Then $I\subseteq \mathrm{\Phi }(\mathrm{\Psi }(I))$.

For $x,y\in L$, one has $\mathrm{\Phi }(x\wedge y)=\mathrm{\Phi }(x)\cap \mathrm{\Phi }(y)$. Also $\mathrm{\Phi }(x\vee y)=\mathrm{\Phi }(x)\cup \mathrm{\Phi }(y)$, because a join-irreducible $j$ satisfies $j\le x\vee y$ exactly when $j\le x$ or $j\le y$ by [L2].

The map $\mathrm{\Phi }$ is injective. If $\mathrm{\Phi }(x)=\mathrm{\Phi }(y)$, then [L1] writes both $x$ and $y$ as the join of the same set of join-irreducibles, so $x=y$.

Conversely, suppose $j\in \mathrm{\Phi }(\mathrm{\Psi }(I))$. If $I=\mathrm{\varnothing }$, then $j\le 0_L$, forcing $j=0_L$, contrary to join-irreducibility. Thus $I$ is nonempty. Repeated application of join-primality [L2] to the finite join $j\le \bigvee I$ gives $j\le i$ for some $i\in I$. Since $I$ is an order ideal, $j\in I$. Hence $\mathrm{\Phi }(\mathrm{\Psi }(I))=I$.

Step 2.3 proves that $\mathrm{\Phi }$ is surjective, while step 2.2 proves injectivity. Step 2.1 shows that it preserves meets and joins. Moreover [L1] gives $\mathrm{\Psi }(\mathrm{\Phi }(x))=x$, so $\mathrm{\Psi }$ is its inverse. Therefore $\mathrm{\Phi }$ is the asserted lattice isomorphism.