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	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfpimbor1.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
	smfpimbor1.a	⊢ 𝐷 = dom 𝐹
	smfpimbor1.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
	smfpimbor1.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
	smfpimbor1.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
	smfpimbor1.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐸 )
Assertion	smfpimbor1	⊢ ( 𝜑 → 𝑃 ∈ ( 𝑆 ↾t 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		smfpimbor1.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		smfpimbor1.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
3		smfpimbor1.a	⊢ 𝐷 = dom 𝐹
4		smfpimbor1.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
5		smfpimbor1.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
6		smfpimbor1.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
7		smfpimbor1.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐸 )
8		eqid	⊢ { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) } = { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) }
9	1 2 3 4 5 6 7 8	smfpimbor1lem2	⊢ ( 𝜑 → 𝑃 ∈ ( 𝑆 ↾t 𝐷 ) )