Theorem issmfdmpt

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

	Ref	Expression
Hypotheses	issmfdmpt.x	|- F/ x ph
	issmfdmpt.a	|- F/ a ph
	issmfdmpt.s	|- ( ph -> S e. SAlg )
	issmfdmpt.i	|- ( ph -> A C_ U. S )
	issmfdmpt.b	|- ( ( ph /\ x e. A ) -> B e. RR )
	issmfdmpt.p	|- ( ( ph /\ a e. RR ) -> { x e. A | B < a } e. ( S |`t A ) )
Assertion	issmfdmpt	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )

Proof

Step	Hyp	Ref	Expression
1		issmfdmpt.x	|- F/ x ph
2		issmfdmpt.a	|- F/ a ph
3		issmfdmpt.s	|- ( ph -> S e. SAlg )
4		issmfdmpt.i	|- ( ph -> A C_ U. S )
5		issmfdmpt.b	|- ( ( ph /\ x e. A ) -> B e. RR )
6		issmfdmpt.p	|- ( ( ph /\ a e. RR ) -> { x e. A | B < a } e. ( S |`t A ) )
7		nfmpt1	|- F/_ x ( x e. A |-> B )
8		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
9	1 5 8	fmptdf	|- ( ph -> ( x e. A |-> B ) : A --> RR )
10		eqidd	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
11	10 5	fvmpt2d	|- ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
12	11	breq1d	|- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) < a <-> B < a ) )
13	12	ex	|- ( ph -> ( x e. A -> ( ( ( x e. A |-> B ) ` x ) < a <-> B < a ) ) )
14	1 13	ralrimi	|- ( ph -> A. x e. A ( ( ( x e. A |-> B ) ` x ) < a <-> B < a ) )
15		rabbi	|- ( A. x e. A ( ( ( x e. A |-> B ) ` x ) < a <-> B < a ) <-> { x e. A | ( ( x e. A |-> B ) ` x ) < a } = { x e. A | B < a } )
16	14 15	sylib	|- ( ph -> { x e. A | ( ( x e. A |-> B ) ` x ) < a } = { x e. A | B < a } )
17	16	adantr	|- ( ( ph /\ a e. RR ) -> { x e. A | ( ( x e. A |-> B ) ` x ) < a } = { x e. A | B < a } )
18	17 6	eqeltrd	|- ( ( ph /\ a e. RR ) -> { x e. A | ( ( x e. A |-> B ) ` x ) < a } e. ( S |`t A ) )
19	7 2 3 4 9 18	issmfdf	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )