Theorem: Integral of Horizontal Section of Measurable Function gives Measurable Function

Let $\struct {X, \Sigma_X, \mu}$ and $\struct {Y, \Sigma_Y, \nu}$ be $\sigma$-finite measure spaces.
Let $f : X \times Y \to \overline \R_{\ge 0}$ be a positive $\Sigma_X \otimes \Sigma_Y$-measurable function, where $\Sigma_X \otimes \Sigma_Y$ is the product $\sigma$-algebra of $\Sigma_X$ and $\Sigma_Y$.
Define the function $g : X \to \overline \R$ by: 
:$\ds \map g y = \int f^y \rd \mu$
where $f^y$ is the $y$-horizontal section of $f$. 
Then: 
:$g$ is $\Sigma_Y$-measurable.

Proof:
First we prove the case of:
:$f = \chi_E$
where $E$ is a $\Sigma_X \otimes \Sigma_Y$-measurable set.
From Horizontal Section of Characteristic Function is Characteristic Function of Horizontal Section, we have: 
:$f^y = \chi_{E^y}$
From Horizontal Section of Measurable Function is Measurable, we also have: 
:$f^y$ is $\Sigma_Y$-measurable.
Since $f \ge 0$, we may take $\mu$-integrals, giving: 
{{begin-eqn}}
{{eqn	| l = \int f^y \rd \mu
		| r = \int \chi_{E^y} \rd \mu
}}
{{eqn	| r = \map {\mu} {E^y}
		| c = Integral of Characteristic Function
}}
{{end-eqn}}
so that: 
:$\map g y = \map {\mu} {E^y}$ for each $y \in Y$.
From Measure of Horizontal Section of Measurable Set gives Measurable Function, we then have: 
:$g$ is $\Sigma_Y$-measurable
in the case that $f$ is a characteristic function.
Now consider the case of positive simple $f$. 
Write the standard representation of $f$ as: 
:$\ds f = \sum_{k \mathop = 1}^n a_k \chi_{E_k}$
with:
:$E_1, E_2, \ldots, E_n$ pairwise disjoint $\Sigma_X \otimes \Sigma_Y$-measurable sets
:$a_1, a_2, \ldots, a_n$ non-negative real numbers.
Then, we have, from Horizontal Section of Simple Function is Simple Function:
:$f^y$ is a positive simple function
with:
:$\ds f^y = \sum_{k \mathop = 1}^n a_k \chi_{\paren {E_k}^y}$
where:
:$\paren {E_1}^y, \paren {E_2}^y, \ldots, \paren {E_n}^y$ are pairwise disjoint $\Sigma_X$-measurable sets
:$a_1, a_2, \ldots, a_n$ non-negative real numbers.
From Simple Function is Measurable, we have: 
:$f$ is $\Sigma_X \otimes \Sigma_Y$-measurable.
From Vertical Section of Measurable Function is Measurable, we also have: 
:$f^y$ is $\Sigma_X$-measurable.
Since $f \ge 0$, we may take $\mu$-integrals, giving:
{{begin-eqn}}
{{eqn	| l = \int f^y \rd \mu
		| r = \int \paren {\sum_{k \mathop = 1}^n a_k \chi_{\paren {E_k}^y} } \rd \mu
}}
{{eqn	| r = \sum_{k \mathop = 1}^n \int \paren {a_k \chi_{\paren {E_k}^y} } \rd \mu
		| c = Integral of Positive Measurable Function is Additive
}}
{{eqn	| r = \sum_{k \mathop = 1}^n a_k \paren {\int \chi_{\paren {E_k}^y} \rd \mu}
		| c = Integral of Positive Measurable Function is Positive Homogeneous
}}
{{eqn	| r = \sum_{k \mathop = 1}^n a_k \map {\mu} {\paren {E_k}^y}
		| c = Integral of Characteristic Function: Corollary
}}
{{end-eqn}}
giving:
:$\ds \map g y = \sum_{k \mathop = 1}^n a_k \map {\mu} {\paren {E_k}^y}$
From Pointwise Sum of Measurable Functions is Measurable: General Result, we have: 
:$g$ is $\Sigma_Y$-measurable
in the case that $f$ is a simple function.
Now take a general positive $\Sigma_X \otimes \Sigma_Y$-measurable function $f$.
From Measurable Function is Pointwise Limit of Simple Functions:
:there exists a increasing sequence of simple functions $\sequence {f_n}_{n \mathop \in \N}$ such that $f_n \to f$.
From Horizontal Section preserves Increasing Sequences of Functions, we have: 
:the sequence $\sequence {\paren {f_n}^y}_{n \mathop \in \N}$ is increasing.
From Horizontal Section preserves Pointwise Limits of Sequences of Functions, we have: 
:$\ds f^y = \lim_{n \mathop \to \infty} \paren {f_n}^y$
From the monotone convergence theorem, we then have: 
:$\ds \map g y = \int f^y \rd \mu = \lim_{n \mathop \to \infty} \int \paren {f_n}^y \rd \mu$
For each $n \in \N$, define the function $g_n : Y \to \overline \R$ by: 
:$\ds \map {g_n} y = \int \paren {f_n}^y \rd \mu$
Since each $f_n$ is a positive simple function, we have that: 
:$\ds \sequence {g_n}_{n \mathop \in \N}$ is a sequence of $\Sigma_X$-measurable functions.
So$g$ is the limit of a sequence of $\Sigma_X$-measurable functions.
Then, from Pointwise Limit of Measurable Functions is Measurable, we have: 
:$g$ is $\Sigma_X$-measurable
for each positive $\Sigma_X \otimes \Sigma_Y$-measurable $f$.
{{qed}}