An equality concerning the Lebesgue integral Let $f:X\mapsto[0,+\infty)$ be a non-negative measurable function defined on the space $X$, endowed with the complete $\sigma$-additive, $\sigma$-finite, measure $\mu$ defined on the $\sigma$-algebra of the measurable subsets of $X$.
I have read that the following equality holds for the Lebesgue integral:
$$\int_X f d\mu = \int_{[0,+\infty)} \mu(\{x\in X: f(x)>t\}) d\mu_t$$where $\mu_t$ is the usual Lebesgue linear measure.
I would like to understand why this equality holds, but I have got serious problems in proving even the measurability of the function $\phi:t\mapsto \mu(\{x\in X: f(x)>t\})$ (necessary for the Lebesgue integral to be defined) to myself, which would be proved if we could verify that, for any $c\in\mathbb{R}$, the set $$\{t\in\mathbb{R}_{\ge 0}:\mu(\{x\in X: f(x)>t\})<c\}$$is measurable. How can we prove the equality (including the measurability of $\phi$)? I $\infty$-ly thank anyone answering.
 A: For measurability: Verify that in your setup (assuming $\mu$ is positive), $t\to \mu(\{f>t\})$ is decreasing on $[0,\infty).$ Then recall that any monotone function on $[0,\infty)$ is Lebesgue measurable there.
For intuition: Consider the graph of some nice positive function $f$ defined on an interval $[a,b].$ Look at the area $\int_a^b f(x)\,dx $ geometrically and you'll see, by slicing horizontally, that it's also equal to $\int_c^d m(\{f>y\})\, dy,$ where $[c,d]$ is the range of $f.$ The picture is helpful here.
A: Uisng Fubini, we have that
\begin{align*}
\int_X fd\mu &= \int_X \int_0^{f(x)}dt d\mu\\
&=\int_X \int_0^{\infty}\mathbb{I}_{\{f(x) > t\}}dt d\mu\\
&=\int_0^{\infty} \int_X \mathbb{I}_{\{f(x) > t\}} d\mu dt\\
&=\int_0^{\infty}\mu(x\in X, f(x) > t) dt.
\end{align*}
Here, for clarity, we use $dt$ to denote the Lebesgue measure.
A: The assumptions that $\mu$ is complete and $\sigma$-finite are not necessary. The result holds for any measure $\mu$.
The answer by zhw shows that the function $\phi$ is measurable, so I won't duplicate that here.
Let's first prove the desired equality assuming that $f$ is a nonnegative, real-valued simple function. In this case, we have
$$f(x) = \sum_{m=1}^{M}a_m \chi_{A_m}(x)$$
where each $a_m$ is in $[0,\infty)$, and the $A_m$'s are pairwise disjoint and  $\mu$-measurable. Observe that for any $t \in [0,\infty)$,
$$\{x \in X : f(x) > t\} = \bigcup_{\{m\ :\ a_m > t\}}A_m$$
so
$$\mu\{x \in X : f(x) > t\} = \sum_{\{m\ :\ a_m > t\}}\mu(A_m) = \sum_{m=1}^{M}\mu(A_m) \chi_{[0,a_m)}(t)$$
Integrating both sides gives us
$$\begin{aligned}
\int_0^{\infty} \mu\{x \in X : f(x) > t\}\ dt
&= \sum_{m=1}^{M}\mu(A_m) \int_0^{\infty}\chi_{[0,a_m)}(t)\ dt\\
&= \sum_{m=1}^{M}\mu(A_m) a_m \\
&= \int f d\mu \\ 
\end{aligned}$$
Therefore the result holds when $f$ is a simple function. To complete the proof for the general case, let $(f_n)$ be an increasing sequence of simple functions which converges pointwise to $f$. For fixed $t$, observe that if $m \leq n$, then
$$\{x \in X : f_m(x) > t\} \subseteq \{x \in X : f_n(x) > t\}$$
Moreover, 
$$\{x \in X : f(x) > t\} = \bigcup_{n=1}^{\infty}\{x \in X : f_n(x) > t\}$$
These two facts imply that
$$\mu \{x \in X : f(x) > t\} = \lim_{n \to \infty}\mu \{x \in X : f_n(x) > t\}$$
We may now apply the monotone convergence theorem (twice) to conclude that
$$\begin{aligned}
\int_X f\ d\mu &=
\int_X \lim_{n \to \infty}f_n\ d\mu \\
&= \lim_{n \to \infty} \int_X f_n\ d\mu \\
&= \lim_{n\to \infty} \int_0^{\infty} \mu \{x \in X : f_n(x) > t\}\ dt \\
&= \int_0^{\infty} \lim_{n \to \infty} \mu \{x \in X : f_n(x) > t\}\ dt \\
&= \int_0^{\infty} \mu\{x \in X : f(x) > t\}\ dt \\
\end{aligned}$$
as desired.
