Question about elementary set theory (related to database design theory) Definition:
Let $U$ and $D$ be sets. For $X, Y \subseteq U$ and $I \subseteq D^U(:=\{f \mid \text{$f$ is a map from $U$ to $D$}\})$, we define an 3-ary predicate $P(I, X, Y)$ as follows:
$$ P(I, X, Y) \text{ if and only if for every $s, t \in I, s|_X = t|_X$ implies $s|_Y = t|_Y$}.$$
Futhermore, for a family $F := \{(X_\lambda, Y_\lambda)\}_{\lambda \in \Lambda}$of pairs of subsets of $U$, we define a predicate $I \vDash F$ as follows:
$$ I \vDash F \text{ if and only if for every $(X, Y) \in F, P(I, X, Y)$}.$$
Question:
Let $U$ be a finite set, $D$ a set, $F :=\{(X_\lambda, Y_\lambda)\}_{\lambda \in \Lambda}$ a finite family of pairs of subsets of $U$, and $a \in U \setminus \cup_{\lambda \in \Lambda} (X_\lambda \cup Y_\lambda)$ and suppose $K (\subseteq U)$ satisfies that for any finite subset $I$ of $D^U$, $I \vDash F$ implies $P(I, K, U)$. Then $a \in K$?
Thank you in advance.

To those who know database design theory:
This question can be explained in the language of database design theory as follows:
$$ \text{
If $a$ is an attribute that does not occur in a set of functional dependencies $F$, does a  superkey $K$ always contain $a$?
}$$
 A: Yes, $a \in K$. If $|D| \leq 1$ it's trivial, so assume $d_0, d_1 \in D$ are distinct. Now let a $K$ be given and take two functions $I = \{f_0, f_1\}$ which agree except that $f_0(a) = d_0 \neq d_1 = f_1(a)$. Then $I \models F$, because $f_0|_Y = f_1|_Y$ holds for any $(X, Y) \in F$ since $a \notin Y$ by definition. It follows that $P(I, K, U)$. Since $f_0|_U = f_0 \neq f_1 = f_1|_U$ it follows that also $f_0|_K \neq f_1|_K$. But then we must have $a \in K$.
A: I was able to prove $a\in K$ by myself, though the proof needs some knowledge of database design theory. I will share the outline of it.

By structural induction on Armstrong's rules, the following proposition can be proven easily.
Proposition: Let $U$ be a attribute set, $F = \{X_\lambda \rightarrow Y_\lambda\}_{\lambda \in \Lambda}$ a set of functional dependencies, and $A \in U \setminus \cup_{\lambda \in \Lambda} Y_\lambda$. Then for any functional dependency $X \rightarrow Y$ that can be derived by Armstrong's rules from  $F$ (hereinafter denote $F \vdash X \rightarrow Y$), $A \in Y$ implies $A \in X$.
Since if $K$ is a superkey, $F \vdash K \rightarrow U$ and $A \in U$,
this proposition leads to what we want easily by the soundness and completeness of Armstrong's rules.
