Please help me prove that the equational definition of Heyting Semilattice is equivalent to the Order-Theoretic definition The situation:
An algebraic semilattice $(L, \wedge, \top)$ satisfies the following axioms:

*

*$\forall x \in L. x \wedge \top = x$

*$\forall x, y \in L. x \wedge y = y \wedge x$

*$\forall x, y, z \in L. (x \wedge y) \wedge z = x \wedge (y \wedge z)$

*$\forall x \in L. x \wedge x = x$
A Heyting semilattice can be defined in two equivalent ways. However, the proof that these definitions are the same is given as an exercise in every book I've read, and I can't figure it out (I'm surely missing something obvious, but I'm stuck).
Definition 1: equational definition.
There is an operation $\implies : L^2 \to L$ satisfying the following axioms:

*

*$\forall x \in L. (x \implies x) = \top$

*$\forall x, y \in L. x \wedge (x \implies y) = x \wedge y$

*$\forall x, y \in L. y \wedge (x \implies y) = y$

*$\forall x, y, z \in L. x \implies (y \wedge z) = (x \implies y) \wedge (x \implies z)$
Definition 2: order definition.
Define the following partial order on $L$:
$\forall x, y \in L. x \le y$ if and only if $x = x \wedge y$
There is an operation $\implies : L^2 \to L$ such that:
$\forall x, y, z \in L. x \wedge y \le z$ if and only if $x \le (y \implies z)$
Does anyone know where I can find a worked-out proof of this result?
 A: Let us give names to the axioms, for reference.
$H$ stands for Heyting.
$(H_0)$ $x\wedge y \leq z \Leftrightarrow x \leq y \to z$.
$(H_1)$ $x\to x = 1$,
$(H_2)$ $x \wedge (x\to y) = x \wedge y$,
$(H_3)$ $(x\to y) \wedge y = y$,
$(H_4)$ $x \to (y \wedge x) = (x\to y) \wedge (x\to z)$.
We want to prove that a $\wedge$-semilattice $H$ with $1$ satisfies $(H_0)$ iff it satisfies $(H_1)-(H_4)$.
Suppose it satisfies $(H_0)$.
Then, for every $a,b \in H$,
$$a \wedge b \leq b \Rightarrow a \leq b \to b.$$
In particular this is true for $a=1$, and so $H$ satisfies $(H_1)$.
For $a,b,c \in H$, from
$$a \to b \leq a \to b$$
we get from $(H_0)$ that
$$a \wedge (a\to b) \leq b;$$
certainly $a \wedge (a\to b) \leq a$, whence $a \wedge (a\to b) \leq a\wedge b$.
Conversely, from
$$a \wedge b = (a \wedge b) \wedge a \leq b,$$
we obtain
$$a \wedge b \leq a \to b;$$
since $a \wedge b \leq a$, it follows that $a \wedge (a\to b) = a\wedge b$, and $H$ satisfies $(H_2)$.
The verification of $(H_3)$ is easier: one inequality is obvious, and the other follows from two applications of $(H_0)$ and equations of semilattices.
To prove $(H_4)$, let $a,b,c \in H$, and use $(H_2)$ to get
$$a \wedge (a \to b) = a \wedge b \leq b$$
and
$$a \wedge (a \to c) = a \wedge c \leq c,$$
whence
$$a \wedge (a\to b) \wedge (a\to c) \leq b \wedge c$$
and from $(H_0)$,
$$(a\to b) \wedge (a\to c) \leq a \to (b \wedge c).$$
For the converse, observe first that $\to$ is order-preserving in the second coordinate:
indeed, if $u \leq v$, then
$$x \wedge u \leq v$$
and from $(H_2)$,
$$(x\to u) \wedge x \leq v$$
and from $(H_0)$,
$$x \to u \leq x \to v.$$
Now it follows that
$$a \to (b \wedge c) \leq a \to b,$$
since $b \wedge c \leq b$ and similarly $a \to (b \wedge c) \leq a \to c$, whence
$$(a\to b) \wedge (a\to c) = a \to (b \wedge c),$$
that is, $H$ satisfies $(H_4)$.
Now we must prove that $H$ satisfies $(H_0)$, whenever it satisfies $(H_1)-(H_4)$.
Start with noting that from $(H_4)$ it follows that $\to$ is, again, order-preserving in the second coordinate (I'll leave that to you).
Let $a,b,c \in H$.
If $a \leq b \to c$, then
$$a \wedge b \leq b \wedge (b \to c) = b \wedge c \leq c.$$
Conversely, if $a \wedge b \leq c$ then
$$b \to (a \wedge b) \leq b \to c,$$
and the result follows from the fact that
$$a = a \wedge (b \to a),$$
whence
$$a \leq b \to a = (b \to a) \wedge (b \to b) = b \to (a \wedge b).$$
(It is not difficult to find which axiom is used in each step.)
