Result on D41: Indicator function
Finite product of indicator functions equals indicator of intersection
Formulation 0
Let $X$ be a D11: Set such that
(i) $E_1, \ldots, E_N \subseteq X$ are each a D78: Subset
Then \begin{equation} \prod_{n = 1}^N I_{E_n} = I_{\bigcap_{n = 1}^N E_n} \end{equation}
Subresults
R4333: Binary product of indicator functions equals indicator of intersection
Formulation 0
Let $X$ be a D11: Set such that
(i) $A, B \subseteq X$ are each a D78: Subset of $X$
Then \begin{equation} I_A I_B = I_{A \cap B} \end{equation}
Proofs
Proof 0
Let $X$ be a D11: Set such that
(i) $E_1, \ldots, E_N \subseteq X$ are each a D78: Subset
We understand both $\prod_{n = 1}^N I_{E_n}$ and $I_{\bigcap_{n = 1}^N E_n}$ as functions from $X$ to $\{ 0, 1 \}$. Since the domain and codomain sets are the same, it suffices to show that they attain the same values on $X$.

If $x \in X$, then one has the following chain of equivalencies \begin{equation} \begin{split} \left( \prod_{n = 1}^N I_{E_n} \right)(x) = I_{E_1}(x) \cdots I_{E_N}(x) = 1 \quad & \iff \quad x \in E_1, \quad \dots, \quad x \in E_N \\ & \iff \quad x \in \bigcap_{n = 1}^N E_n \\ & \iff \quad I_{\bigcap_{n = 1}^N}(x) = 1 \\ \end{split} \end{equation} The claim then follows from R2965: Indicator function is uniquely identified by its support. $\square$