Theorem issmfle2d

Description: A sufficient condition for " F being a measurable function w.r.t. to the sigma-algebra S ". (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	issmfle2d.a	|- F/ a ph
	issmfle2d.s	|- ( ph -> S e. SAlg )
	issmfle2d.d	|- ( ph -> D C_ U. S )
	issmfle2d.f	|- ( ph -> F : D --> RR )
	issmfle2d.l	|- ( ( ph /\ a e. RR ) -> ( `' F " ( -oo (,] a ) ) e. ( S |`t D ) )
Assertion	issmfle2d	|- ( ph -> F e. ( SMblFn ` S ) )

Proof

Step	Hyp	Ref	Expression
1		issmfle2d.a	|- F/ a ph
2		issmfle2d.s	|- ( ph -> S e. SAlg )
3		issmfle2d.d	|- ( ph -> D C_ U. S )
4		issmfle2d.f	|- ( ph -> F : D --> RR )
5		issmfle2d.l	|- ( ( ph /\ a e. RR ) -> ( `' F " ( -oo (,] a ) ) e. ( S |`t D ) )
6	4	adantr	|- ( ( ph /\ a e. RR ) -> F : D --> RR )
7		rexr	|- ( a e. RR -> a e. RR* )
8	7	adantl	|- ( ( ph /\ a e. RR ) -> a e. RR* )
9	6 8	preimaiocmnf	|- ( ( ph /\ a e. RR ) -> ( `' F " ( -oo (,] a ) ) = { x e. D | ( F ` x ) <_ a } )
10	9 5	eqeltrrd	|- ( ( ph /\ a e. RR ) -> { x e. D | ( F ` x ) <_ a } e. ( S |`t D ) )
11	1 2 3 4 10	issmfled	|- ( ph -> F e. ( SMblFn ` S ) )