How is Fubini's theorem used in the following proof? I'm having trouble to understand exactly how we are using Fubini's theorem in the following proof involving the distribution function, since it newer explicitly involves an integral with product measure.
The proof is given to show that we can calculate an integral over some measure space $X $ as an integral over $[0, \infty ]$
$$\int _X (\phi \circ f ) d \mu= \int _0 ^{\infty } \mu \{f > t \} \phi '(t) dt$$
Where $(X, \mu ) $ is a $\sigma $-finite measure space, and $\phi :[0, \infty ] \mapsto [0, \infty ]$ is monotonic and absolutely continuous on $[0, T ]$
The proof consits of constructing a set $E $ consisting of all points $(x,t) $ where $f> t $. It is easily shown that this set is measurable with respect to the product measure on $X \times [0, \infty ] $. Further the t-section $E^t $ is measurable with respect ot $\mu $.
The distribution function of $f $ is $\mu(E^t )= \int _X \chi _E (x,t) d \mu (x) $
And the right side of the top equality is equal to $\int _0 ^{\infty } \mu (E^t) \phi '(t) dt= \int _X d \mu \int \chi _E (x,t) \phi '(t) d t  $
By Fubini's theorem? 

Exactly how are we using Fubini's theorem as there is no explicit use of an  integral with respect to the product measure. I can see that a part of the conclusion in Fubini's theorem is used to conclude that $\mu (E^t) $ is measurable with respect to the measure on $[0, \infty ]$. Is that all?
Thanks in advance!
 A: You missed the hypothesis that $\phi(0)=0$ and that $f\geqslant0$ almost everywhere, then, for every nonnegative $s$, $$\phi(s)=\int_0^s\phi'(t)\mathrm dt=\int_0^\infty\phi'(t)\mathbf 1_{s\gt t}\mathrm dt.$$ Now, $f(x)\geqslant0$ for $\mu$-almost every $x$ hence $$\phi\circ f(x)=\int_0^\infty\phi'(t)\mathbf 1_{f(x)\gt t}\mathrm dt.$$ Integrating both sides with respect to $\mu$ and interverting, thanks to Tonelli theorem applied to the product measure $\mu\otimes\mathrm{Leb}$ on $X\times[0,\infty)$, the integral on $X$ with respect to $\mu$ and the integral on $[0,\infty)$ with respect to $\mathrm{Leb}$, one gets $$\int_X\phi\circ f(x)\mathrm d\mu(x)=\int_X\left(\int_0^\infty\phi'(t)\mathbf 1_{f(x)\gt t}\mathrm dt\right)\mathrm d\mu(x)=\int_0^\infty\phi'(t)\left(\int_X\mathbf 1_{f(x)\gt t}\mathrm d\mu(x)\right)\mathrm dt,$$ and the proof is complete since, for every $t$, the inner parenthesis on the RHS is $\mu\{f\gt t\}$.
A: The $\sigma$-additivity assumption on $(X,\mathscr{F},\mu)$ can be relaxed. Here is a slightly more general result:
Theorem: Suppose  $\nu$ is a positive Radon measure on $[0,\infty)$, and let  $f$ be a nonnegative  measurable function on $X$. If $\{f>0\}$ is $\sigma$-finite w.r.t. $\mu$,
$$
\begin{align}
\int_X\nu\Big(\big[0,f(x)\big)\Big)\,\mu(dx)=\int^\infty_0\mu(\{f>t\})\,\nu(dt)\tag{1}\label{fubini2}
\end{align}
$$
In particular, if $\varphi$ is a function on $[0,\infty)$ with $\varphi(0)=0$ , that is absolutely continuous in compact subsets of $[0,\infty)$, and $\nu(dx)=\varphi'(x)\,dx$,  then
$$
\begin{align}
\int_X(\varphi\circ f)\,d\mu=\int^\infty_0\mu(\{f>t\})\varphi'(t)dt.\tag{2}\label{fubini3}
\end{align}
$$
Here is short proof:
Since $f\in\mathscr{M}^+(\mu)$ and $\{f>0\}$ is $\mu$ $\sigma$--finite,  the set  $E=\{(x,t)\in X\times[0,\infty): f(x)>t\}\in\mathscr{M}(\nu\otimes\mu)$ is $\sigma$--finite. By Fubini's theorem
$$
\begin{align}
\int^\infty_0\mu(E^t)\,\nu(dt)=
\int_{X\times[0,\infty)}\mathbb{1}_E(x,t)\,
 \mu\otimes\nu(dx, dt)
=\int_X\nu(E_x)\,\mu(dx)
\end{align}
$$
and $\eqref{fubini2}$ follows.
In the special case where $\varphi$ is a function that is absolutely continuous function in compact subintervals  of $[0,\infty)$ and $\varphi(0)=0$, the fundamental theorem of Calculus implies that  $\nu([0,f(x)))=\int^{f(x)}_0\varphi'(t)\,dt=\varphi(f(x))$, and $\eqref{fubini3}$ follows.
