I want to prove (source: Dugundji, Topology):
$$\bigcap_{p}\prod_{\alpha}A_{\alpha,p}=\prod_{a}\bigcap_{p} A_{\alpha,p}$$
Proof:
$$
\begin{align}
x \in \bigcap_{p}\prod_{\alpha}A_{\alpha,p}
&\iff \forall p: x \in \prod_{\alpha}A_{\alpha,p} \\
&\iff \forall p, i: x_i \in A_{\alpha_{i}, p} \\
&\iff \forall i: x_i \in A_{\alpha_{i},p} \\
&\iff x \in \prod_{\alpha}\bigcap_{p}A_{\alpha,p}
\end{align}
$$
Steps 1 and 3 I am pretty confident about because that is a by definition of intersection, and exchanging order of universal quantification. I am not sure if I utilized the definition of product correctly.
My book defines a product as:
$\prod_{\alpha}A_{\alpha,p} = \{c:\mathcal{A} \to \bigcup_{\alpha}A_{\alpha} \mid \forall \alpha \in \mathcal{A}, c(\alpha) \in A_{\alpha}\}$
The proof seems reasonable to me based on the 'coordinate' intution of a product, but maybe it should be more detailed to utilize the given definition?
Best Answer
Let's first think about the definition of the cartesian product you gave. I claim that it is just a formalization of the intuitive notion that you have in mind. Namely, an element of $\prod_{\alpha \in \mathcal{A}} A_{\alpha}$ should be an "$\mathcal{A}$-indexed tuple" $(x_{\alpha})$, with each $x_{\alpha} \in A_{\alpha}$. But what is the precise definition of such a tuple? One way of thinking of it is as assigning to every $\alpha$ an element of $A_{\alpha}$; in other words, it's a map $x \colon \mathcal{A} \to \bigcup_{\alpha} A_{\alpha}$ such that $x(\alpha) \in A_{\alpha}$ for every $\alpha$. We are then free to use the notation $(x_{\alpha})_{\alpha \in \mathcal{A}}$ for this map and think in terms of the coordinates $x_{\alpha} := x(\alpha)$. See e.g. this question for more details.
Now, with this out of the way, let's look at your proof of the purported equality
$$ \bigcap_{\rho} \prod_{\alpha} A_{\alpha, \rho} = \prod_{\alpha} \bigcap_{\rho} A_{\alpha, \rho} $$
(which is a direct generalization of the fact that $A \times B \cap A' \times B' = (A \cap A') \times (B \cap B')$). You're right insofar as the main point is exchanging the $\forall$ quantifiers. Formally, however, your proof doesn't make sense (why does $i$ appear, and where did $\rho$ go after the 3rd step?). I'll try to reformulate it.
An element of the left-hand side is a tuple $(x_{\alpha})$ such that $$ \forall \rho : (x_{\alpha}) \in \prod_{\alpha} A_{\alpha, \rho}, $$ i.e. (using the definition of the cartesian product) $$ \forall \rho\ \forall \alpha : x_{\alpha} \in A_{\alpha, \rho}. $$ But that's just saying $$ \forall \alpha\ \forall \rho : x_{\alpha} \in A_{\alpha, \rho}, $$ which is equivalent to $(x_{\alpha})$ lying in the right-hand side.
Lastly, here's a technical point that I swept under the rug: In order for the equality above to literally be true, depending on your set-theoretic implementation of maps, we need the check that the codomains of the maps representing the tuples agree. But that's not a problem here, because it is assumed (as this exercise is an extension of Theorem 9.5) that for each $\alpha$ there is a set $Y_{\alpha}$ containing every $A_{\alpha, \rho}$. Hence we can just represent the tuples by maps $\mathcal{A} \to \bigcup_{\alpha} Y_{\alpha}$.