Welcome to MSE!
Unfortunately, it is not true that the meet of two join-irreducible elements is always join-irreducible. For a simple example, consider:
here $d$ and $e$ are both join irreducible, but their meet is not.
The "standard" proof (that is, the proof that I am most familiar with) of Birkhoff's theorem goes as follows:
First, show that join-irreducible elements act like primes, in the following sense:
If $p$ is join-irreducible, and $p \leq a_1 \lor a_2 \lor \cdots \lor a_n$, then actually $p \leq a_i$ for some $i$.
This is where we (heavily) use distributivity of our lattice. It is analogous to the statement
"If $p$ is prime, and $p \mid a_1 \times a_2 \times \cdots \times a_n$ then actually $p \mid a_i$ for some $i$".
Next, we show that every element of our lattice can be "factored" into join-irreducibles. This is where we heavily use finiteness of our lattice (a chain condition would work for this lemma too). You will need the first lemma while proving it.
Each $x$ can be written uniquely as a irredundant join of join-irreducible elements.
This is analogous to the unique factorization of some integer into primes.
Finally, we consider the map $\varphi : L \to L(J(L))$ given by
$$\varphi(x) = \{p \in J(L) ~|~ p \leq x\}$$
Can you show that this map is an isomorphism?
Edit:
It is worth noting that we can go the other way as well. Instead of sending $L \to L(J(L))$, we can send a poset $P$ to $J(L(P))$ by $\psi(y) = \langle y \rangle$. This is also an isomorphism!
This information together shows that $\varphi$ and $\psi$ actually form an Equivalence of Categories between the category of finite posets (with monotone maps) and the category of finite distributive lattices (with bounded homomorphisms). For more information, see this wikipedia page.
I hope this helps! ^_^
You have a lot of information there and perhaps you can savage some of it to give a proof.
I'll take a different approach.
Start by proving the following lemma:
Lemma. Let $P$ be a finite set. Then
- The map $\Phi:P \to \mathcal J(\mathcal O(P))$ given by $x \mapsto {\downarrow}x$ is an order-isomorphism.
- The map $\Psi : P \to \mathcal M(\mathcal O(P))$ given by $x \mapsto P \setminus {\downarrow}x$ is an order-isomorphism.
Hence
\begin{equation}
\label{equation}
P \cong \mathcal J(\mathcal O(P)) \cong \mathcal M(\mathcal O(P)).
\tag{$\dagger$}
\end{equation}
Now, by Birkhoff's Theorem, for a finite distributive lattice $L$ we have that $L \cong \mathcal O(\mathcal J(L))$.
As $\mathcal O(P)$ is distributive for any $P$ (and obviously finite if $P$ is),
\begin{align}
\mathcal J(L)
&\cong \mathcal J(\mathcal O(\mathcal J(L))) \tag{Theorem of Birkhoff}\\
&\cong \mathcal M(\mathcal O(\mathcal J(L))) \tag{by \eqref{equation}}\\
&\cong \mathcal M(L). \tag{Theorem of Birkhoff}
\end{align}
Best Answer
An Heyting algebra is a bounded lattice $L$ such that, for every pair $a,b\in L$ there is an element $(a\Rightarrow b)\in L$ such that $$a\wedge x\leqslant b\leftrightarrow x\leqslant(a\Rightarrow b)$$In particular, you can see that $a\Rightarrow b$ is the sup of the set $$A=\{x\in L|a\wedge x\leqslant b\}$$ In the case of a finite lattice, $A=\{x_1,\cdots,x_n\}$, so there is a sup $$s=x_1\vee\cdots\vee x_n$$ to prove that $a\wedge s\leqslant b$ just use that $L$ is a distributive lattice, so $$a\wedge\bigvee_ix_i=\bigvee_ia\wedge x_i\leqslant b$$