Theorem smfpimltxrmpt

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021) (Revised by Glauco Siliprandi, 20-Dec-2024)

	Ref	Expression
Hypotheses	smfpimltxrmpt.x	⊢ Ⅎ 𝑥 𝜑
	smfpimltxrmpt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfpimltxrmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	smfpimltxrmpt.f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
	smfpimltxrmpt.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
Assertion	smfpimltxrmpt	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∈ ( 𝑆 ↾t 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		smfpimltxrmpt.x	⊢ Ⅎ 𝑥 𝜑
2		smfpimltxrmpt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfpimltxrmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4		smfpimltxrmpt.f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
5		smfpimltxrmpt.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
6		nfcv	⊢ Ⅎ 𝑥 𝐴
7	1 6 2 3 4 5	smfpimltxrmptf	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∈ ( 𝑆 ↾t 𝐴 ) )