I’ve found the following counter-example, to this conjecture:

Example For a set $S$ of binary relations

$\forall X_0,\dots,X_n\in S:\mathrm{up}(X_0\sqcap^{\mathsf{FCD}}\dots\sqcap^{\mathsf{FCD}} X_n)\subseteq S$

does not imply that there exists funcoid $f$ such that $S=\mathrm{up}\, f$.

The proof is currently available at this PDF file and this wiki page.

I start the “research-in-the middle” project (an outlaw offspring of Polymath Project) introducing to your attention the following conjecture:

Conjecture The following are equivalent (for every lattice $\mathsf{FCD}$ of funcoids between some sets and a set $S$ of principal funcoids (=binary relations)):

1. $\forall X, Y \in S : \mathrm{up} (X \sqcap^{\mathsf{FCD}} Y) \subseteq S$.
2. $\forall X_0,\dots,X_n \in S : \mathrm{up} (X \sqcap^{\mathsf{FCD}} \dots \sqcap^{\mathsf{FCD}} X_n) \subseteq S$ (for every natural $n$).
3. There exists a funcoid $f\in\mathsf{FCD}$ such that $S=\mathrm{up}\, f$.

$3\Rightarrow 2$ and $2\Rightarrow 1$ are obvious.

I welcome you to actively participate in the research!

I have found a surprisingly easy proof of this conjecture which I proposed yesterday.

Theorem Let $S$ be a set of binary relations. If for every $X, Y \in S$ we have $\mathrm{up} (X \sqcap^{\mathsf{FCD}} Y) \subseteq S$ then there exists a funcoid $f$ such that $S = \mathrm{up}\, f$.

The proof (currently available in this PDF file) is based on “Funcoids are filters” chapter of my book.

Conjecture Let $S$ be a set of binary relations. If for every $X, Y \in S$ we have $\mathrm{up} (X \sqcap^{\mathsf{FCD}} Y) \subseteq S$ then there exists a funcoid $f$ such that $S = \mathrm{up}\, f$.

The converse of this theorem does not hold.

Counterexample: Take $S = \mathrm{up}\, \mathrm{id}^{\mathsf{FCD}}_{\Omega}$. We know that $S$ is not a filter base. But it is trivial to prove that $S$ is a base of the funcoid $\mathrm{id}^{\mathsf{FCD}}_{\Omega}$.

Definition A set $S$ of binary relations is a base of a funcoid $f$ when all elements of $S$ are above $f$ and $\forall X \in \mathrm{up}\, f \exists T \in S : T \sqsubseteq X$.

It was easy to show:

Proposition A set $S$ of binary relations is a base of a funcoid iff it is a base of $\bigsqcap^{\mathsf{FCD}} S$.

Today I’ve proved the following important theorem:

Theorem If $S$ is a filter base on the set of funcoids then $S$ is a base of $\bigsqcap^{\mathsf{FCD}} S$.

The proof is currently located in this PDF file.

It is yet unknown whether the converse theorem holds, that is whether every base of a funcoid is a filter base on the set of funcoids.

I’ve proved the following (for every funcoids $f$ and $g$):

Statement $\mathrm{up}\, (f \sqcap^{\mathsf{FCD}} g) \subseteq \bigcup \{ \mathrm{up}\, (F \sqcap^{\mathsf{FCD}} G) \mid F \in \mathrm{up}\, f, G \in \mathrm{up}\, g \}$ or equivalently: If $Z\in\mathrm{up}\, (f \sqcap^{\mathsf{FCD}} g)$ then there exists $F \in \mathrm{up}\, f$, $G \in \mathrm{up}\, g$ such that $Z\in\mathrm{up}\, (F \sqcap^{\mathsf{FCD}} G)$.

But now I’ve noticed that the proof was with an error! So it is again a conjecture.