Metamath Proof Explorer

Theorem smfres

Description: The restriction of sigma-measurable function is sigma-measurable. Proposition 121E (h) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfres.s 
|- ( ph -> S e. SAlg )
smfres.f 
|- ( ph -> F e. ( SMblFn ` S ) )
smfres.a 
|- ( ph -> A e. V )
Assertion smfres 
|- ( ph -> ( F |` A ) e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smfres.s 
 |-  ( ph -> S e. SAlg )
2 smfres.f 
 |-  ( ph -> F e. ( SMblFn ` S ) )
3 smfres.a 
 |-  ( ph -> A e. V )
4 nfv 
 |-  F/ a ph
5 inss1 
 |-  ( dom F i^i A ) C_ dom F
6 5 a1i 
 |-  ( ph -> ( dom F i^i A ) C_ dom F )
7 eqid 
 |-  dom F = dom F
8 1 2 7 smfdmss 
 |-  ( ph -> dom F C_ U. S )
9 6 8 sstrd 
 |-  ( ph -> ( dom F i^i A ) C_ U. S )
10 1 2 7 smff 
 |-  ( ph -> F : dom F --> RR )
11 fresin 
 |-  ( F : dom F --> RR -> ( F |` A ) : ( dom F i^i A ) --> RR )
12 10 11 syl 
 |-  ( ph -> ( F |` A ) : ( dom F i^i A ) --> RR )
13 ovexd 
 |-  ( ( ph /\ a e. RR ) -> ( S |`t dom F ) e. _V )
14 3 adantr 
 |-  ( ( ph /\ a e. RR ) -> A e. V )
15 1 adantr 
 |-  ( ( ph /\ a e. RR ) -> S e. SAlg )
16 2 adantr 
 |-  ( ( ph /\ a e. RR ) -> F e. ( SMblFn ` S ) )
17 mnfxr 
 |-  -oo e. RR*
18 17 a1i 
 |-  ( ( ph /\ a e. RR ) -> -oo e. RR* )
19 rexr 
 |-  ( a e. RR -> a e. RR* )
20 19 adantl 
 |-  ( ( ph /\ a e. RR ) -> a e. RR* )
21 15 16 7 18 20 smfpimioo 
 |-  ( ( ph /\ a e. RR ) -> ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) )
22 eqid 
 |-  ( ( `' F " ( -oo (,) a ) ) i^i A ) = ( ( `' F " ( -oo (,) a ) ) i^i A )
23 13 14 21 22 elrestd 
 |-  ( ( ph /\ a e. RR ) -> ( ( `' F " ( -oo (,) a ) ) i^i A ) e. ( ( S |`t dom F ) |`t A ) )
24 10 ffund 
 |-  ( ph -> Fun F )
25 respreima 
 |-  ( Fun F -> ( `' ( F |` A ) " ( -oo (,) a ) ) = ( ( `' F " ( -oo (,) a ) ) i^i A ) )
26 24 25 syl 
 |-  ( ph -> ( `' ( F |` A ) " ( -oo (,) a ) ) = ( ( `' F " ( -oo (,) a ) ) i^i A ) )
27 26 eqcomd 
 |-  ( ph -> ( ( `' F " ( -oo (,) a ) ) i^i A ) = ( `' ( F |` A ) " ( -oo (,) a ) ) )
28 27 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( ( `' F " ( -oo (,) a ) ) i^i A ) = ( `' ( F |` A ) " ( -oo (,) a ) ) )
29 12 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( F |` A ) : ( dom F i^i A ) --> RR )
30 29 20 preimaioomnf 
 |-  ( ( ph /\ a e. RR ) -> ( `' ( F |` A ) " ( -oo (,) a ) ) = { x e. ( dom F i^i A ) | ( ( F |` A ) ` x ) < a } )
31 28 30 eqtr2d 
 |-  ( ( ph /\ a e. RR ) -> { x e. ( dom F i^i A ) | ( ( F |` A ) ` x ) < a } = ( ( `' F " ( -oo (,) a ) ) i^i A ) )
32 2 dmexd 
 |-  ( ph -> dom F e. _V )
33 restco 
 |-  ( ( S e. SAlg /\ dom F e. _V /\ A e. V ) -> ( ( S |`t dom F ) |`t A ) = ( S |`t ( dom F i^i A ) ) )
34 1 32 3 33 syl3anc 
 |-  ( ph -> ( ( S |`t dom F ) |`t A ) = ( S |`t ( dom F i^i A ) ) )
35 34 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( ( S |`t dom F ) |`t A ) = ( S |`t ( dom F i^i A ) ) )
36 35 eqcomd 
 |-  ( ( ph /\ a e. RR ) -> ( S |`t ( dom F i^i A ) ) = ( ( S |`t dom F ) |`t A ) )
37 31 36 eleq12d 
 |-  ( ( ph /\ a e. RR ) -> ( { x e. ( dom F i^i A ) | ( ( F |` A ) ` x ) < a } e. ( S |`t ( dom F i^i A ) ) <-> ( ( `' F " ( -oo (,) a ) ) i^i A ) e. ( ( S |`t dom F ) |`t A ) ) )
38 23 37 mpbird 
 |-  ( ( ph /\ a e. RR ) -> { x e. ( dom F i^i A ) | ( ( F |` A ) ` x ) < a } e. ( S |`t ( dom F i^i A ) ) )
39 4 1 9 12 38 issmfd 
 |-  ( ph -> ( F |` A ) e. ( SMblFn ` S ) )