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 $\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 $\Phi$ is well defined.

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

For $x,y\in L$, one has $\Phi(x\wedge y)=\Phi(x)\cap\Phi(y)$. Also $\Phi(x\vee y)=\Phi(x)\cup\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 $\Phi$ is injective. If $\Phi(x)=\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\Phi(\Psi(I))$. If $I=\varnothing$, then $j\le0_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 $\Phi(\Psi(I))=I$.

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