@John wrote:

> Suppose we have a poset \$$\mathcal{V}\$$ with all joins, and a doubly indexed family of elements in \$$\mathcal{V}\$$, say \$$\lbrace v_{a b} \rbrace_{a \in A, b \in B} \$$ where \$$A\$$ and \$$B\$$ are arbitrary sets. Then

> $\bigvee_{a \in A} \bigvee_{b \in B} v_{ab} = \bigvee_{a \in A, b \in B} v_{ab} = \bigvee_{b \in B} \bigvee_{a \in A} v_{ab}$

> It takes a bit of work to show this, but it seems so obvious I don't have the energy right now. All three are just different ways of thinking about the least upper bound of all the elements \$$v_{a b}\$$.

Thinking about this further has led me to the conclusion that I'm overthinking it! I take your point that even if we were to index or structure our sets \$$A\$$, \$$B\$$, the _join_ would ignore that structure (since joins do not care about order or repetition).

Regarding proving the "obvious" identity, here's one reasonably slick way of doing it.

We write \$$(\downarrow v)\$$ for the subset \$$\\{ x \in \mathcal{V} : x \leq v\\}\$$.

We can then write the definition of join as

$\bigvee S \leq v \iff S \subseteq (\downarrow v)$

But this just states that \$$\bigvee\$$ is left adjoint to \$$\downarrow\$$ (treating them as monotone maps between \$$\mathcal{V}\$$ and the poset of subsets of \$$\mathcal{V}\$$).

So \$$\bigvee\$$ preserves joins, ie \$$\bigvee \bigcup \\{ S_i : i \in I \\} = \bigvee \\{ \bigvee S_i : i \in I \\}\$$.

which is what we need to show that the join of all \$$v_{a b}\$$ = the join of the joins of its rows = the join of the joins of its columns.