Theorem issmfgtd

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	issmfgtd.a	|- F/ a ph
	issmfgtd.s	|- ( ph -> S e. SAlg )
	issmfgtd.d	|- ( ph -> D C_ U. S )
	issmfgtd.f	|- ( ph -> F : D --> RR )
	issmfgtd.p	|- ( ( ph /\ a e. RR ) -> { x e. D | a < ( F ` x ) } e. ( S |`t D ) )
Assertion	issmfgtd	|- ( ph -> F e. ( SMblFn ` S ) )

Proof

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