Theorem smfpimbor1

Description: Given a sigma-measurable function, the preimage of a Borel set belongs to the subspace sigma-algebra induced by the domain of the function. Proposition 121E (f) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfpimbor1.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	smfpimbor1.f	$$⊢\phi \to F\in \mathrm{SMblFn}\left(S\right)$$
	smfpimbor1.a	$$⊢D=\mathrm{dom}F$$
	smfpimbor1.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	smfpimbor1.b	$$⊢B=\mathrm{SalGen}\left(J\right)$$
	smfpimbor1.e	$$⊢\phi \to E\in B$$
	smfpimbor1.p	$$⊢P=F^{-1}\left[E\right]$$
Assertion	smfpimbor1	$$⊢\phi \to P\in \left(S{\upharpoonright }_{𝑡}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		smfpimbor1.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
2		smfpimbor1.f	$$⊢\phi \to F\in \mathrm{SMblFn}\left(S\right)$$
3		smfpimbor1.a	$$⊢D=\mathrm{dom}F$$
4		smfpimbor1.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
5		smfpimbor1.b	$$⊢B=\mathrm{SalGen}\left(J\right)$$
6		smfpimbor1.e	$$⊢\phi \to E\in B$$
7		smfpimbor1.p	$$⊢P=F^{-1}\left[E\right]$$
8		eqid	$$⊢\left\{e\in 𝒫ℝ|F^{-1}\left[e\right]\in \left(S{\upharpoonright }_{𝑡}D\right)\right\}=\left\{e\in 𝒫ℝ|F^{-1}\left[e\right]\in \left(S{\upharpoonright }_{𝑡}D\right)\right\}$$
9	1 2 3 4 5 6 7 8	smfpimbor1lem2	$$⊢\phi \to P\in \left(S{\upharpoonright }_{𝑡}D\right)$$