Applying results

(i)	R2369: Expressing a countably infinite pointwise sum of indicator functions in terms of set cardinality
(ii)	R1242: Unsigned basic integral is compatible with measure
(iii)	R1232: Tonelli's theorem for sums and integrals

we have \begin{equation} \begin{split} \int_X \# \{ n \in \mathbb{N} : x \in E_n \} \, \mu(d x) & = \int_X \sum_{n \in \mathbb{N}} I_{E_n}(x) \, \mu(d x) \\ & = \sum_{n \in \mathbb{N}} \int_X I_{E_n}(x) \, \mu(d x) = \sum_{n \in \mathbb{N}} \mu(E_n) \end{split} \end{equation} Since the function $x \mapsto \# \{ n \in \mathbb{N} : x \in E_n \}$ is thus integrable on $M$, then result R1237: Unsigned basic Borel function almost everywhere finite if integral is finite states that $\# \{ n \in \mathbb{N} : x \in E_n \} < \infty$ for almost every $x \in X$. That is, the set $\{ n \in \mathbb{N} : x \in E_n \}$ is finite for almost every $x \in X$. Conversely, the set $\{ n \in \mathbb{N} : x \in E_n \}$ is nonfinite only on a set of measure zero so that we have \begin{equation} \mu(\{ x \in X : \# \{ n \in \mathbb{N} : x \in E_n \} = \infty \}) = 0 \end{equation} We can now use R2371: Equivalent characterisations of membership in a limit superior for sequences of sets to connect the two claims so that we have \begin{equation} \mu \left( \bigcap_{n = 1}^{\infty} \bigcup_{m = n}^{\infty} E_m \right) = \mu(\{ x \in X : \# \{ n \in \mathbb{N} : x \in E_n \} = \infty \}) = 0 \end{equation} $\square$