Metamath Proof Explorer

Theorem issmfdf

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

Proof

Step Hyp Ref Expression
1 issmfdf.x 
 |-  F/_ x F
2 issmfdf.a 
 |-  F/ a ph
3 issmfdf.s 
 |-  ( ph -> S e. SAlg )
4 issmfdf.d 
 |-  ( ph -> D C_ U. S )
5 issmfdf.f 
 |-  ( ph -> F : D --> RR )
6 issmfdf.p 
 |-  ( ( ph /\ a e. RR ) -> { x e. D | ( F ` x ) < a } e. ( S |`t D ) )
7 5 fdmd 
 |-  ( ph -> dom F = D )
8 7 4 eqsstrd 
 |-  ( ph -> dom F C_ U. S )
9 5 ffdmd 
 |-  ( ph -> F : dom F --> RR )
10 1 nfdm 
 |-  F/_ x dom F
11 nfcv 
 |-  F/_ x D
12 10 11 rabeqf 
 |-  ( dom F = D -> { x e. dom F | ( F ` x ) < a } = { x e. D | ( F ` x ) < a } )
13 7 12 syl 
 |-  ( ph -> { x e. dom F | ( F ` x ) < a } = { x e. D | ( F ` x ) < a } )
14 7 oveq2d 
 |-  ( ph -> ( S |`t dom F ) = ( S |`t D ) )
15 13 14 eleq12d 
 |-  ( ph -> ( { x e. dom F | ( F ` x ) < a } e. ( S |`t dom F ) <-> { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) )
16 15 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 ) ) )
17 6 16 mpbird 
 |-  ( ( ph /\ a e. RR ) -> { x e. dom F | ( F ` x ) < a } e. ( S |`t dom F ) )
18 17 ex 
 |-  ( ph -> ( a e. RR -> { x e. dom F | ( F ` x ) < a } e. ( S |`t dom F ) ) )
19 2 18 ralrimi 
 |-  ( ph -> A. a e. RR { x e. dom F | ( F ` x ) < a } e. ( S |`t dom F ) )
20 8 9 19 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 ) ) )
21 eqid 
 |-  dom F = dom F
22 1 3 21 issmff 
 |-  ( 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 ) ) ) )
23 20 22 mpbird 
 |-  ( ph -> F e. ( SMblFn ` S ) )