5
$\begingroup$

I found an interesting exercise of other amazing book (Jech's) that I'm not totally sure about how to do it.

Prove the following form of the distributive law:

$$\bigcap_{a\in A} \bigg(\, \bigcup_{b\in B} F_{a,b} \, \bigg) = \bigcup_{f\in ^AB} \bigg(\, \bigcap_{a \in A} F_{a,f(a)}\,\bigg) $$

Assuming that $F_{a,b_1} \cap F_{a,b_2} = \emptyset $ for each $a\in A$ and $b_1,b_2\in B$ and $b_1\not=b_2$.

First of all, I'm not completely sure about what $ F_{a,b}$ really means. I suppose that is the range of a family with a domain $A \times B$.

And second, I cannot figure out how to do the converse (assuming that the first part it is correct, I used as normal in this kind of proof element chasing)

Proof:

($\Rightarrow$) ...

($\Leftarrow$) Suppose that $z\in \bigcup_{f\in ^AB} \big(\, \bigcap_{a \in A} F_{a,f(a)}\,\big)$; then there is $f\in \,^AB$ such that $z\in \bigcap_{a \in A} F_{a,f(a)}\, $. Let $a \in A$ be arbitrary.

Claim 1 $\, \bigcap_{a \in A} F_{a,f(a)}\subseteq F_{a,f(a)} \subseteq \bigcup_{b\in B} F_{a,b}$.

Proof of the Claim 1:

For the first inclusion: Suppose $z\in\bigcap_{a \in A} F_{a,f(a)}$; then for each $a\in A$ we have that $z\in F_{a,f(a)}$. Then $\bigcap_{a \in A} F_{a,f(a)}\subseteq F_{a,f(a)}$. For the second inclusion: Now suppose $z\in F_{a,f(a)}$. Clearly $f(a)\in B$ because $f\in ^AB$. Then there is some $b\in B$ such that $z\in F_{a,b}$ and hence that $z\in \bigcup_{b\in B} F_{a,b}$. $\square$

Since $a$ was arbitrary it follows that $z\in \bigcup_{b\in B} F_{a,b}$ (by claim 1) for each $a\in A$ and hence that $z\in \bigcap_{a\in A} \big(\, \bigcup_{b\in B} F_{a,b} \, \big)$ as desired.

I really, really would very much appreciate some help with that. Thanks in advance as usual.

$\endgroup$
  • $\begingroup$ How can you possibly have proved anything if you are not sure what $F_{a,b}$ means? $\endgroup$ – Mariano Suárez-Álvarez Aug 20 '13 at 4:29
  • $\begingroup$ I suppose that is the family $\left\{ F_{a,b}\right\}$ with domain $A\times B$. But to be honest I'm not completely sure. I assumed that. $\endgroup$ – Jose Antonio Aug 20 '13 at 4:35
3
$\begingroup$

Your understanding of $F_{a,b}$ is correct.

Your statement of Claim $1$ is a bit flawed, because you’re using the letter $a$ both as an index variable in the intersection and as a specific element of $A$. You should instead let $a_0\in A$ be arbitrary, and state the claim as follows:

Claim $\mathbf1$ : $\bigcap_{a\in A}F_{a,f(a)}\subseteq F_{a_0,f(a_0)}\subseteq \bigcup_{b\in B}F_{a_0,b}$.

Your argument for the first inclusion is then just the observation that an intersection of sets is contained in any one of those sets: if $z\in\bigcap_{a\in A}F_{a,f(a)}$, then $z\in F_{a,f(a)}$ for each $a\in A$, and in particular $z\in F_{a_0,f(a_0)}$. For the second inclusion you will of course then start with $z\in F_{a_0,f(a_0)}$, and the rest of your argument proceeds with only very minor changes: $f(a_0)\in B$, so $F_{a_0,f(a_0)}\subseteq\bigcup_{b\in B}F_{a_0,b}$.

Now you can argue that since $a_0\in A$ was arbitrary, for each $a\in A$ we have $z\in\bigcup_{b\in B}F_{a,b}$, and therefore $z\in\bigcap_{a\in A}\bigcup_{b\in B}F_{a,b}$, as desired.

In other words, your argument is basically correct, but you’ve allowed yourself to confuse generic elements with specific elements; a trivial rewriting takes care of the problem.

For the other direction, suppose that $z\in\bigcap_{a\in A}\bigcup_{b\in B}F_{a,b}$. Let $a\in A$ be arbitrary; then $z\in\bigcup_{b\in B}F_{a,b}$, so there is a $b\in B$ such that $z\in F_{a,b}$. The disjointness condition on the sets ensures that this $b$ is unique, so $\{\langle a,b\rangle\in A\times B:z\in F_{a,b}\}$ is actually a function from $A$ to $B$; call this function $f_z$. Clearly $z\in\bigcap_{a\in A}F_{a,f_z(a)}\subseteq\bigcup_{f\in{}^BA}\bigcap_{a\in A}F_{a,f(a)}$, and you’re done.

$\endgroup$
  • $\begingroup$ I'll try to pay more attention to the use of generic elements with specific elements. But this $\{\langle a,b\rangle\in A\times B:z\in F_{a,b}\}$ it was breaking my head. Thank you so much :) $\endgroup$ – Jose Antonio Aug 20 '13 at 4:56
  • $\begingroup$ @Jose: Yes, finding a nice way to express that function is a little tricky. You’re welcome! $\endgroup$ – Brian M. Scott Aug 20 '13 at 5:03
0
$\begingroup$

Like in many set theory proofs, it helps to translate from the set level to the element level, and then use ordinary logic.

In this case that means that we are asked to prove for any $\;z\;$ that $$ (0) \;\;\; \langle \forall a :: \langle \exists b :: z \in F(a,b) \rangle \rangle \;\equiv\; \langle \exists f : f \in A \to B : \langle \forall a :: z \in F(a,f(a)) \rangle \rangle $$ (Throughout this answer implicitly $\;a \in A\;$ and $\;b,b_1,b_2 \in B\;$, and $\;f\;$ is a function.)

It seems necessary to prove both directions separately.

The first thing I tried is start from the most complex side of $(0)$, and push the $\;\exists f\;$ inward as much as possible: for any $\;z\;$, \begin{align} & \langle \exists f : f \in A \to B : \langle \forall a :: z \in F(a,f(a)) \rangle \rangle \\ \Rightarrow & \;\;\;\;\;\text{"logic: $\;\exists\forall \Rightarrow \forall\exists\;$"} \\ & \langle \forall a :: \langle \exists f : f \in A \to B : z \in F(a,f(a)) \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"introduce abbreviation with one-point rule -- suggested by left hand side of $(0)$"} \\ & \langle \forall a :: \langle \exists f : f \in A \to B : \langle \exists b : b = f(a) : z \in F(a,b) \rangle \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"move $\;\exists f\;$ to the only part which uses $\;f\;$"} \\ & \langle \forall a :: \langle \exists b : \langle \exists f : f \in A \to B : b = f(a) \rangle : z \in F(a,b) \rangle \rangle \\ \Rightarrow & \;\;\;\;\;\text{"weaken range of $\;\exists b\;$ to $\;\text{true}\;$"} \\ & \langle \forall a :: \langle \exists b :: z \in F(a,b) \rangle \rangle \\ \end{align} This proves the backward direction of $(0)$.

For the forward direction we assume $$ (1) \;\;\; \langle \forall a :: \langle \exists b :: z \in F(a,b) \rangle \rangle $$ and we must construct a function $\;f\ \in A \to B\;$ such that $\;\langle \forall a :: z \in F(a,f(a)) \rangle\;$. We calculate for any function $\;f\;$ and any $\;z\;$ \begin{align} & \langle \forall a :: z \in F(a,f(a)) \rangle \\ \equiv & \;\;\;\;\;\text{"rewrite using one-point rule -- allows definition of function application"} \\ & \langle \forall a,b : b = f(a) : z \in F(a,b) \rangle \\ \equiv & \;\;\;\;\;\text{"definition of function application"} \\ & \langle \forall a,b : (a,b) \in f : z \in F(a,b) \rangle \\ \Leftarrow & \;\;\;\;\;\text{"the simplest possible choice for $\;f\;$"} \\ & f = \{a,b : z \in F(a,b) : (a,b)\} \end{align} (Notation. The last line describes the set which, for each $\;a,b\;$ such that $\;z \in F(a,b)\;$, contains the pair $\;(a,b)\;$.)

Now we only have to prove that this relation is indeed a function from $\;A \to B\;$. It clearly is a subset of $\;A \times B\;$, since $\;a \in A\;$ and $\;b \in B\;$ (implicitly). And it is a function, since for any $\;z\;$ \begin{align} & \{a,b : z \in F(a,b) : (a,b)\}\text{ is a function} \\ \equiv & \;\;\;\;\;\text{"definition of what it means to be a function"} \\ & \langle \forall a :: \langle \exists! b :: z \in F(a,b) \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"split $\;\exists! b\;$ into $\;\exists b\;$ and $\;! b\;$; $\;\land\;$ distributes over $\;\forall\;$"} \\ & \langle \forall a :: \langle \exists b :: z \in F(a,b) \rangle \rangle \;\land\; \langle \forall a :: \langle ! b :: z \in F(a,b) \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"left part using $(1)$; right part using $(2)$ below"} \\ & \text{true} \end{align} (Notation. Here $\;! b\;$ means "there exists at most one $\;b\;$.)

The right part of the last step follows directly from the proviso, which (translated to the element level) says that $$ \langle \forall a, b_1, b_2 : b_1 \not= b_2 : \lnot(z \in F(a,b_1) \land z \in F(a,b_2)) \rangle $$ or equivalently $$ (2) \;\;\; \langle \forall a :: \langle ! b :: z \in F(a,b) \rangle \rangle $$ for any $\;z\;$.

This completes the proof.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.