Theorem smfpreimaltf

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)

	Ref	Expression
Hypotheses	smfpreimaltf.x	|- F/_ x F
	smfpreimaltf.s	|- ( ph -> S e. SAlg )
	smfpreimaltf.f	|- ( ph -> F e. ( SMblFn ` S ) )
	smfpreimaltf.d	|- D = dom F
	smfpreimaltf.a	|- ( ph -> A e. RR )
Assertion	smfpreimaltf	|- ( ph -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )

Proof

Step	Hyp	Ref	Expression
1		smfpreimaltf.x	|- F/_ x F
2		smfpreimaltf.s	|- ( ph -> S e. SAlg )
3		smfpreimaltf.f	|- ( ph -> F e. ( SMblFn ` S ) )
4		smfpreimaltf.d	|- D = dom F
5		smfpreimaltf.a	|- ( ph -> A e. RR )
6	1 2 4	issmff	|- ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) )
7	3 6	mpbid	|- ( ph -> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) )
8	7	simp3d	|- ( ph -> A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) )
9		breq2	|- ( a = A -> ( ( F ` x ) < a <-> ( F ` x ) < A ) )
10	9	rabbidv	|- ( a = A -> { x e. D | ( F ` x ) < a } = { x e. D | ( F ` x ) < A } )
11	10	eleq1d	|- ( a = A -> ( { x e. D | ( F ` x ) < a } e. ( S |`t D ) <-> { x e. D | ( F ` x ) < A } e. ( S |`t D ) ) )
12	11	rspcva	|- ( ( A e. RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
13	5 8 12	syl2anc	|- ( ph -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )