Metamath Proof Explorer

Theorem smfco

Description: The composition of a Borel sigma-measurable function with a sigma-measurable function, is sigma-measurable. Proposition 121E (g) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfco.s 
|- ( ph -> S e. SAlg )
smfco.f 
|- ( ph -> F e. ( SMblFn ` S ) )
smfco.j 
|- J = ( topGen ` ran (,) )
smfco.b 
|- B = ( SalGen ` J )
smfco.h 
|- ( ph -> H e. ( SMblFn ` B ) )
Assertion smfco 
|- ( ph -> ( H o. F ) e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smfco.s 
 |-  ( ph -> S e. SAlg )
2 smfco.f 
 |-  ( ph -> F e. ( SMblFn ` S ) )
3 smfco.j 
 |-  J = ( topGen ` ran (,) )
4 smfco.b 
 |-  B = ( SalGen ` J )
5 smfco.h 
 |-  ( ph -> H e. ( SMblFn ` B ) )
6 nfv 
 |-  F/ a ph
7 cnvimass 
 |-  ( `' F " dom H ) C_ dom F
8 7 a1i 
 |-  ( ph -> ( `' F " dom H ) C_ dom F )
9 eqid 
 |-  dom F = dom F
10 1 2 9 smfdmss 
 |-  ( ph -> dom F C_ U. S )
11 8 10 sstrd 
 |-  ( ph -> ( `' F " dom H ) C_ U. S )
12 retop 
 |-  ( topGen ` ran (,) ) e. Top
13 3 12 eqeltri 
 |-  J e. Top
14 13 a1i 
 |-  ( ph -> J e. Top )
15 14 4 salgencld 
 |-  ( ph -> B e. SAlg )
16 eqid 
 |-  dom H = dom H
17 15 5 16 smff 
 |-  ( ph -> H : dom H --> RR )
18 17 ffund 
 |-  ( ph -> Fun H )
19 1 2 9 smff 
 |-  ( ph -> F : dom F --> RR )
20 19 ffund 
 |-  ( ph -> Fun F )
21 18 20 funcofd 
 |-  ( ph -> ( H o. F ) : ( `' F " dom H ) --> ran H )
22 17 frnd 
 |-  ( ph -> ran H C_ RR )
23 21 22 fssd 
 |-  ( ph -> ( H o. F ) : ( `' F " dom H ) --> RR )
24 cnvco 
 |-  `' ( H o. F ) = ( `' F o. `' H )
25 24 imaeq1i 
 |-  ( `' ( H o. F ) " ( -oo (,) a ) ) = ( ( `' F o. `' H ) " ( -oo (,) a ) )
26 23 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( H o. F ) : ( `' F " dom H ) --> RR )
27 rexr 
 |-  ( a e. RR -> a e. RR* )
28 27 adantl 
 |-  ( ( ph /\ a e. RR ) -> a e. RR* )
29 26 28 preimaioomnf 
 |-  ( ( ph /\ a e. RR ) -> ( `' ( H o. F ) " ( -oo (,) a ) ) = { x e. ( `' F " dom H ) | ( ( H o. F ) ` x ) < a } )
30 imaco 
 |-  ( ( `' F o. `' H ) " ( -oo (,) a ) ) = ( `' F " ( `' H " ( -oo (,) a ) ) )
31 30 a1i 
 |-  ( ( ph /\ a e. RR ) -> ( ( `' F o. `' H ) " ( -oo (,) a ) ) = ( `' F " ( `' H " ( -oo (,) a ) ) ) )
32 25 29 31 3eqtr3a 
 |-  ( ( ph /\ a e. RR ) -> { x e. ( `' F " dom H ) | ( ( H o. F ) ` x ) < a } = ( `' F " ( `' H " ( -oo (,) a ) ) ) )
33 17 adantr 
 |-  ( ( ph /\ a e. RR ) -> H : dom H --> RR )
34 33 28 preimaioomnf 
 |-  ( ( ph /\ a e. RR ) -> ( `' H " ( -oo (,) a ) ) = { x e. dom H | ( H ` x ) < a } )
35 15 adantr 
 |-  ( ( ph /\ a e. RR ) -> B e. SAlg )
36 5 adantr 
 |-  ( ( ph /\ a e. RR ) -> H e. ( SMblFn ` B ) )
37 simpr 
 |-  ( ( ph /\ a e. RR ) -> a e. RR )
38 35 36 16 37 smfpreimalt 
 |-  ( ( ph /\ a e. RR ) -> { x e. dom H | ( H ` x ) < a } e. ( B |`t dom H ) )
39 34 38 eqeltrd 
 |-  ( ( ph /\ a e. RR ) -> ( `' H " ( -oo (,) a ) ) e. ( B |`t dom H ) )
40 15 elexd 
 |-  ( ph -> B e. _V )
41 5 dmexd 
 |-  ( ph -> dom H e. _V )
42 elrest 
 |-  ( ( B e. _V /\ dom H e. _V ) -> ( ( `' H " ( -oo (,) a ) ) e. ( B |`t dom H ) <-> E. e e. B ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) )
43 40 41 42 syl2anc 
 |-  ( ph -> ( ( `' H " ( -oo (,) a ) ) e. ( B |`t dom H ) <-> E. e e. B ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) )
44 43 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( ( `' H " ( -oo (,) a ) ) e. ( B |`t dom H ) <-> E. e e. B ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) )
45 39 44 mpbid 
 |-  ( ( ph /\ a e. RR ) -> E. e e. B ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) )
46 imaeq2 
 |-  ( ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) = ( `' F " ( e i^i dom H ) ) )
47 46 3ad2ant3 
 |-  ( ( ph /\ e e. B /\ ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) = ( `' F " ( e i^i dom H ) ) )
48 ovexd 
 |-  ( ( ph /\ e e. B ) -> ( S |`t dom F ) e. _V )
49 2 elexd 
 |-  ( ph -> F e. _V )
50 cnvexg 
 |-  ( F e. _V -> `' F e. _V )
51 imaexg 
 |-  ( `' F e. _V -> ( `' F " dom H ) e. _V )
52 49 50 51 3syl 
 |-  ( ph -> ( `' F " dom H ) e. _V )
53 52 adantr 
 |-  ( ( ph /\ e e. B ) -> ( `' F " dom H ) e. _V )
54 1 adantr 
 |-  ( ( ph /\ e e. B ) -> S e. SAlg )
55 2 adantr 
 |-  ( ( ph /\ e e. B ) -> F e. ( SMblFn ` S ) )
56 simpr 
 |-  ( ( ph /\ e e. B ) -> e e. B )
57 eqid 
 |-  ( `' F " e ) = ( `' F " e )
58 54 55 9 3 4 56 57 smfpimbor1 
 |-  ( ( ph /\ e e. B ) -> ( `' F " e ) e. ( S |`t dom F ) )
59 eqid 
 |-  ( ( `' F " e ) i^i ( `' F " dom H ) ) = ( ( `' F " e ) i^i ( `' F " dom H ) )
60 48 53 58 59 elrestd 
 |-  ( ( ph /\ e e. B ) -> ( ( `' F " e ) i^i ( `' F " dom H ) ) e. ( ( S |`t dom F ) |`t ( `' F " dom H ) ) )
61 inpreima 
 |-  ( Fun F -> ( `' F " ( e i^i dom H ) ) = ( ( `' F " e ) i^i ( `' F " dom H ) ) )
62 20 61 syl 
 |-  ( ph -> ( `' F " ( e i^i dom H ) ) = ( ( `' F " e ) i^i ( `' F " dom H ) ) )
63 62 adantr 
 |-  ( ( ph /\ e e. B ) -> ( `' F " ( e i^i dom H ) ) = ( ( `' F " e ) i^i ( `' F " dom H ) ) )
64 2 dmexd 
 |-  ( ph -> dom F e. _V )
65 restabs 
 |-  ( ( S e. SAlg /\ ( `' F " dom H ) C_ dom F /\ dom F e. _V ) -> ( ( S |`t dom F ) |`t ( `' F " dom H ) ) = ( S |`t ( `' F " dom H ) ) )
66 1 8 64 65 syl3anc 
 |-  ( ph -> ( ( S |`t dom F ) |`t ( `' F " dom H ) ) = ( S |`t ( `' F " dom H ) ) )
67 66 eqcomd 
 |-  ( ph -> ( S |`t ( `' F " dom H ) ) = ( ( S |`t dom F ) |`t ( `' F " dom H ) ) )
68 67 adantr 
 |-  ( ( ph /\ e e. B ) -> ( S |`t ( `' F " dom H ) ) = ( ( S |`t dom F ) |`t ( `' F " dom H ) ) )
69 60 63 68 3eltr4d 
 |-  ( ( ph /\ e e. B ) -> ( `' F " ( e i^i dom H ) ) e. ( S |`t ( `' F " dom H ) ) )
70 69 3adant3 
 |-  ( ( ph /\ e e. B /\ ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) -> ( `' F " ( e i^i dom H ) ) e. ( S |`t ( `' F " dom H ) ) )
71 47 70 eqeltrd 
 |-  ( ( ph /\ e e. B /\ ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) e. ( S |`t ( `' F " dom H ) ) )
72 71 3exp 
 |-  ( ph -> ( e e. B -> ( ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) e. ( S |`t ( `' F " dom H ) ) ) ) )
73 72 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( e e. B -> ( ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) e. ( S |`t ( `' F " dom H ) ) ) ) )
74 73 rexlimdv 
 |-  ( ( ph /\ a e. RR ) -> ( E. e e. B ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) e. ( S |`t ( `' F " dom H ) ) ) )
75 45 74 mpd 
 |-  ( ( ph /\ a e. RR ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) e. ( S |`t ( `' F " dom H ) ) )
76 32 75 eqeltrd 
 |-  ( ( ph /\ a e. RR ) -> { x e. ( `' F " dom H ) | ( ( H o. F ) ` x ) < a } e. ( S |`t ( `' F " dom H ) ) )
77 6 1 11 23 76 issmfd 
 |-  ( ph -> ( H o. F ) e. ( SMblFn ` S ) )