Theorem issmfled

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

	Ref	Expression
Hypotheses	issmfled.a	|- F/ a ph
	issmfled.s	|- ( ph -> S e. SAlg )
	issmfled.d	|- ( ph -> D C_ U. S )
	issmfled.f	|- ( ph -> F : D --> RR )
	issmfled.6	|- ( ( ph /\ a e. RR ) -> { x e. D | ( F ` x ) <_ a } e. ( S |`t D ) )
Assertion	issmfled	|- ( ph -> F e. ( SMblFn ` S ) )

Proof

Step	Hyp	Ref	Expression
1		issmfled.a	|- F/ a ph
2		issmfled.s	|- ( ph -> S e. SAlg )
3		issmfled.d	|- ( ph -> D C_ U. S )
4		issmfled.f	|- ( ph -> F : D --> RR )
5		issmfled.6	|- ( ( ph /\ a e. RR ) -> { x e. D | ( F ` x ) <_ a } e. ( S |`t D ) )
6	4	fdmd	|- ( ph -> dom F = D )
7	6 3	eqsstrd	|- ( ph -> dom F C_ U. S )
8	4	ffdmd	|- ( ph -> F : dom F --> RR )
9	6	rabeqdv	|- ( ph -> { x e. dom F | ( F ` x ) <_ a } = { x e. D | ( F ` x ) <_ a } )
10	6	oveq2d	|- ( ph -> ( S |`t dom F ) = ( S |`t D ) )
11	9 10	eleq12d	|- ( ph -> ( { x e. dom F | ( F ` x ) <_ a } e. ( S |`t dom F ) <-> { x e. D | ( F ` x ) <_ a } e. ( S |`t D ) ) )
12	11	adantr	|- ( ( ph /\ a e. RR ) -> ( { x e. dom F | ( F ` x ) <_ a } e. ( S |`t dom F ) <-> { x e. D | ( F ` x ) <_ a } e. ( S |`t D ) ) )
13	5 12	mpbird	|- ( ( ph /\ a e. RR ) -> { x e. dom F | ( F ` x ) <_ a } e. ( S |`t dom F ) )
14	13	ex	|- ( ph -> ( a e. RR -> { x e. dom F | ( F ` x ) <_ a } e. ( S |`t dom F ) ) )
15	1 14	ralrimi	|- ( ph -> A. a e. RR { x e. dom F | ( F ` x ) <_ a } e. ( S |`t dom F ) )
16	7 8 15	3jca	|- ( ph -> ( dom F C_ U. S /\ F : dom F --> RR /\ A. a e. RR { x e. dom F | ( F ` x ) <_ a } e. ( S |`t dom F ) ) )
17		eqid	|- dom F = dom F
18	2 17	issmfle	|- ( ph -> ( F e. ( SMblFn ` S ) <-> ( dom F C_ U. S /\ F : dom F --> RR /\ A. a e. RR { x e. dom F | ( F ` x ) <_ a } e. ( S |`t dom F ) ) ) )
19	16 18	mpbird	|- ( ph -> F e. ( SMblFn ` S ) )