Proof of Restricting a Measure to a Measurable Set

Write $\rho=\mu|_{\mathcal{F}_{Y}}$. Every member of $\mathcal{F}$ is a subset of $X$, as $\mathcal{F}\subseteq\mathcal{P}(X)$ by σ-Algebra and Measurable Space (i), with $\mathcal{P}(X)$ (and likewise $\mathcal{P}(Y)$) the power set; unions $\bigcup_{m\in\mathbb{N}}A_{m}$ of sequences are those of Indexed Families of Sets and Their Union, Intersection and Product (ii). In particular $Y\subseteq X$, so $X\cap Y=Y$. A sequence in $\mathcal{F}_{Y}$ is also a sequence in $\mathcal{F}$, since its range is contained in $\mathcal{F}_{Y}\subseteq\mathcal{F}$.

Proof of (i). By Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (vi), applied to the $\sigma$-algebra $\mathcal{F}_{Y}$ on $Y$ of Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (xi), $\emptyset\in\mathcal{F}_{Y}$, and $\rho(\emptyset)=\mu(\emptyset)=0$ by Measure, Measure Space, and Probability Measure (i). Let $(A_{m})$ be a sequence in $\mathcal{F}_{Y}$ of pairwise disjoint sets. Then $\bigcup_{m\in\mathbb{N}}A_{m}\in\mathcal{F}_{Y}$ by σ-Algebra and Measurable Space (i), and $(A_{m})$ is a pairwise disjoint sequence in $\mathcal{F}$, so by Measure, Measure Space, and Probability Measure (i)

$$\rho\Bigl(\bigcup_{m\in\mathbb{N}}A_{m}\Bigr)=\mu\Bigl(\bigcup_{m\in\mathbb{N}}A_{m}\Bigr)=\sum_{m\in\mathbb{N}}\mu(A_{m})=\sum_{m\in\mathbb{N}}\rho(A_{m}),$$

the sums being those of Sum of a Sequence in [0,∞] (ii), and the last equality holding because the sequences $m\mapsto\mu(A_{m})$ and $m\mapsto\rho(A_{m})$ have the same terms and are therefore equal. Hence $\rho$ is a measure on $(Y,\mathcal{F}_{Y})$ by Measure, Measure Space, and Probability Measure (i).

Proof of (ii). By (i), $\rho$ is a measure on $(Y,\mathcal{F}_{Y})$. Further $Y\in\mathcal{F}_{Y}$ by σ-Algebra and Measurable Space (i), and $\rho(Y)=\mu(Y)$; so if $\mu(Y)<\infty$, then $\rho(Y)<\infty$ and $\rho$ is finite by Measure, Measure Space, and Probability Measure (iii).

Proof of (iii). Let $g$ be the map $A\mapsto A\cap Y$ of Sequences and Maps of Sets: Complements, Traces, Two-Term Sequences, the Disjointing Sequence, and Sequences in a Subset (ii), with $\mathcal{F}$ in place of $\mathcal{A}$. It is a map $\mathcal{F}\to\mathcal{P}(Y)$. For $A\in\mathcal{F}$, $g(A)=A\cap Y\in\mathcal{F}$ by Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (ix); as every element of $\operatorname{ran}g$ is such a value, $\operatorname{ran}g\subseteq\mathcal{F}$, so $g$ is a map $\mathcal{F}\to\mathcal{F}$ by Functions, Values of a Function, and Functions from One Class to Another (iii), and $\nu=\mu\circ g$ is a map $\mathcal{F}\to[0,\infty]$ with $\nu(A)=\mu(A\cap Y)$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii)); it is the only map with these values (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)). We have $\nu(\emptyset)=\mu(\emptyset\cap Y)=\mu(\emptyset)=0$ by Measure, Measure Space, and Probability Measure (i). Let $(A_{m})$ be a sequence in $\mathcal{F}$ of pairwise disjoint sets. By Sequences and Maps of Sets: Complements, Traces, Two-Term Sequences, the Disjointing Sequence, and Sequences in a Subset (ii), applied with the set $\mathcal{F}$ in place of $Z$, there is exactly one sequence $(C_{m})$ in $\mathcal{P}(Y)$ with $C_{m}=A_{m}\cap Y$ for every $m\in\mathbb{N}$. Each $C_{m}$ lies in $\mathcal{F}$ by Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (ix) and satisfies $C_{m}\subseteq Y$, so $C_{m}\in\mathcal{F}_{Y}$; as $\mathcal{F}_{Y}\subseteq\mathcal{P}(Y)$, $(C_{m})$ is a sequence in $\mathcal{F}_{Y}$ by Sequences and Maps of Sets: Complements, Traces, Two-Term Sequences, the Disjointing Sequence, and Sequences in a Subset (v), applied to the set $Y$, and hence a sequence in $\mathcal{F}$. Its terms are pairwise disjoint, since $C_{m}\subseteq A_{m}$ for every $m$ (Monotone Sequences of Sets, Unions of Traces, and Disjointness of Smaller Sets (v)), and $\bigcup_{m\in\mathbb{N}}C_{m}=\bigl(\bigcup_{m\in\mathbb{N}}A_{m}\bigr)\cap Y$ (Monotone Sequences of Sets, Unions of Traces, and Disjointness of Smaller Sets (iii)). By Measure, Measure Space, and Probability Measure (i) applied to $(C_{m})$,

$$\nu\Bigl(\bigcup_{m\in\mathbb{N}}A_{m}\Bigr)=\mu\Bigl(\bigcup_{m\in\mathbb{N}}C_{m}\Bigr)=\sum_{m\in\mathbb{N}}\mu(C_{m})=\sum_{m\in\mathbb{N}}\nu(A_{m}),$$

the last equality because $\mu(C_{m})=\mu(A_{m}\cap Y)=\nu(A_{m})$ for every $m$, so the two sequences of terms are equal. Hence $\nu$ is a measure on $(X,\mathcal{F})$ by Measure, Measure Space, and Probability Measure (i).

Proof of (iv). As $X\in\mathcal{F}$ by σ-Algebra and Measurable Space (i) and $X\cap Y=Y$, we have $\nu(X)=\mu(X\cap Y)=\mu(Y)$.

Proof of (v). By Measure, Measure Space, and Probability Measure (iv) there is a sequence $(X_{m})$ in $\mathcal{F}$ with $\bigcup_{m\in\mathbb{N}}X_{m}=X$ and $\mu(X_{m})<\infty$ for every $m\in\mathbb{N}$. For each $m$, $X_{m}\cap Y\in\mathcal{F}$ by Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (ix), and $X_{m}\cap Y\subseteq X_{m}$, so $\nu(X_{m})=\mu(X_{m}\cap Y)\le\mu(X_{m})$ by Basic Properties of a Measure (iii), so $\nu(X_{m})<\infty$ (Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (iii)). So the sequence $(X_{m})$ shows that $\nu$ is $\sigma$-finite, by Measure, Measure Space, and Probability Measure (iv). For $\rho$, let $(D_{m})$ be the sequence in $\mathcal{P}(Y)$ with $D_{m}=X_{m}\cap Y$ for every $m\in\mathbb{N}$, given by Sequences and Maps of Sets: Complements, Traces, Two-Term Sequences, the Disjointing Sequence, and Sequences in a Subset (ii). By the same argument as for $(C_{m})$ in the proof of (iii), with $X_{m}$ in place of $A_{m}$ (which does not use disjointness), $(D_{m})$ is a sequence in $\mathcal{F}_{Y}$ and $\bigcup_{m\in\mathbb{N}}D_{m}=\bigl(\bigcup_{m\in\mathbb{N}}X_{m}\bigr)\cap Y=X\cap Y=Y$. Moreover $\rho(D_{m})=\mu(X_{m}\cap Y)=\nu(X_{m})<\infty$ for every $m$. So $(D_{m})$ shows that $\rho$ is $\sigma$-finite on $(Y,\mathcal{F}_{Y})$, by Measure, Measure Space, and Probability Measure (iv).