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	|- F/ x ph
	smfpimltxrmpt.s	|- ( ph -> S e. SAlg )
	smfpimltxrmpt.b	|- ( ( ph /\ x e. A ) -> B e. V )
	smfpimltxrmpt.f	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
	smfpimltxrmpt.r	|- ( ph -> R e. RR* )
Assertion	smfpimltxrmpt	|- ( ph -> { x e. A | B < R } e. ( S |`t A ) )

Proof

Step	Hyp	Ref	Expression
1		smfpimltxrmpt.x	|- F/ x ph
2		smfpimltxrmpt.s	|- ( ph -> S e. SAlg )
3		smfpimltxrmpt.b	|- ( ( ph /\ x e. A ) -> B e. V )
4		smfpimltxrmpt.f	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
5		smfpimltxrmpt.r	|- ( ph -> R e. RR* )
6		nfcv	|- F/_ x A
7	1 6 2 3 4 5	smfpimltxrmptf	|- ( ph -> { x e. A | B < R } e. ( S |`t A ) )