Intersection of product is product of intersection 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?
 A: 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}$.
A: Let's show something similar. Suppose $(J_i)_{i\in I}$ is a family of (inhabited) sets and $(A_{i,j})_{j\in J_i}$ are families of sets for every $i\in I$. Then
$$\prod_{i\in I}\bigcap_{j\in J_i}A_{i,j}=\bigcap_{f\in\prod_{i\in I}J_i}\prod_{i\in I}A_{i,f(i)}$$
where for a family of sets $(X_i)_{i\in I}$, their product is
$$\prod_{i\in I}X_i=\left\{f:I\to\bigcup_{i\in I}X_i:f(i)\in X_i,\forall i\in I\right\}.$$
Proof:\begin{align}
 f\in LHS&\iff\forall i\in I\forall j\in J_i.f(i)\in A_{i,j}\\
 &\implies\forall g\in\prod_{i\in I}J_i\forall i\in I.f(i)\in A_{i,g(i)}
\end{align}
as $\bigcap_{j\in J_i}A_{i,j}\subseteq A_{i,g(i)}$.
Other direction: Let $g\in RHS$. By $\mathsf{AC}$, suppose $f\in\prod_{i\in I}J_i$. For any $i\in I$ and any $j\in J_i$, $f_j$ being $f$ with $f(i)=j$ is a choice function so $f(i)\in A_{i,f_j(i)}$ for all $i\in I$ implies $f(i)\in A_{i,j}$ for any $j\in J_i$, for any $i\in I$.
