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 fco3 
 |-  ( 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 23 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( H o. F ) : ( `' F " dom H ) --> RR )
25 rexr 
 |-  ( a e. RR -> a e. RR* )
26 25 adantl 
 |-  ( ( ph /\ a e. RR ) -> a e. RR* )
27 24 26 preimaioomnf 
 |-  ( ( ph /\ a e. RR ) -> ( `' ( H o. F ) " ( -oo (,) a ) ) = { x e. ( `' F " dom H ) | ( ( H o. F ) ` x ) < a } )
28 27 eqcomd 
 |-  ( ( ph /\ a e. RR ) -> { x e. ( `' F " dom H ) | ( ( H o. F ) ` x ) < a } = ( `' ( H o. F ) " ( -oo (,) a ) ) )
29 cnvco 
 |-  `' ( H o. F ) = ( `' F o. `' H )
30 29 imaeq1i 
 |-  ( `' ( H o. F ) " ( -oo (,) a ) ) = ( ( `' F o. `' H ) " ( -oo (,) a ) )
31 30 a1i 
 |-  ( ( ph /\ a e. RR ) -> ( `' ( H o. F ) " ( -oo (,) a ) ) = ( ( `' F o. `' H ) " ( -oo (,) a ) ) )
32 imaco 
 |-  ( ( `' F o. `' H ) " ( -oo (,) a ) ) = ( `' F " ( `' H " ( -oo (,) a ) ) )
33 32 a1i 
 |-  ( ( ph /\ a e. RR ) -> ( ( `' F o. `' H ) " ( -oo (,) a ) ) = ( `' F " ( `' H " ( -oo (,) a ) ) ) )
34 28 31 33 3eqtrd 
 |-  ( ( ph /\ a e. RR ) -> { x e. ( `' F " dom H ) | ( ( H o. F ) ` x ) < a } = ( `' F " ( `' H " ( -oo (,) a ) ) ) )
35 17 adantr 
 |-  ( ( ph /\ a e. RR ) -> H : dom H --> RR )
36 35 26 preimaioomnf 
 |-  ( ( ph /\ a e. RR ) -> ( `' H " ( -oo (,) a ) ) = { x e. dom H | ( H ` x ) < a } )
37 36 eqcomd 
 |-  ( ( ph /\ a e. RR ) -> { x e. dom H | ( H ` x ) < a } = ( `' H " ( -oo (,) a ) ) )
38 37 eqcomd 
 |-  ( ( ph /\ a e. RR ) -> ( `' H " ( -oo (,) a ) ) = { x e. dom H | ( H ` x ) < a } )
39 15 adantr 
 |-  ( ( ph /\ a e. RR ) -> B e. SAlg )
40 5 adantr 
 |-  ( ( ph /\ a e. RR ) -> H e. ( SMblFn ` B ) )
41 simpr 
 |-  ( ( ph /\ a e. RR ) -> a e. RR )
42 39 40 16 41 smfpreimalt 
 |-  ( ( ph /\ a e. RR ) -> { x e. dom H | ( H ` x ) < a } e. ( B |`t dom H ) )
43 38 42 eqeltrd 
 |-  ( ( ph /\ a e. RR ) -> ( `' H " ( -oo (,) a ) ) e. ( B |`t dom H ) )
44 15 elexd 
 |-  ( ph -> B e. _V )
45 5 dmexd 
 |-  ( ph -> dom H e. _V )
46 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 ) ) )
47 44 45 46 syl2anc 
 |-  ( ph -> ( ( `' H " ( -oo (,) a ) ) e. ( B |`t dom H ) <-> E. e e. B ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) )
48 47 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 ) ) )
49 43 48 mpbid 
 |-  ( ( ph /\ a e. RR ) -> E. e e. B ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) )
50 imaeq2 
 |-  ( ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) = ( `' F " ( e i^i dom H ) ) )
51 50 3ad2ant3 
 |-  ( ( ph /\ e e. B /\ ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) = ( `' F " ( e i^i dom H ) ) )
52 ovexd 
 |-  ( ( ph /\ e e. B ) -> ( S |`t dom F ) e. _V )
53 2 elexd 
 |-  ( ph -> F e. _V )
54 cnvexg 
 |-  ( F e. _V -> `' F e. _V )
55 53 54 syl 
 |-  ( ph -> `' F e. _V )
56 imaexg 
 |-  ( `' F e. _V -> ( `' F " dom H ) e. _V )
57 55 56 syl 
 |-  ( ph -> ( `' F " dom H ) e. _V )
58 57 adantr 
 |-  ( ( ph /\ e e. B ) -> ( `' F " dom H ) e. _V )
59 1 adantr 
 |-  ( ( ph /\ e e. B ) -> S e. SAlg )
60 2 adantr 
 |-  ( ( ph /\ e e. B ) -> F e. ( SMblFn ` S ) )
61 simpr 
 |-  ( ( ph /\ e e. B ) -> e e. B )
62 eqid 
 |-  ( `' F " e ) = ( `' F " e )
63 59 60 9 3 4 61 62 smfpimbor1 
 |-  ( ( ph /\ e e. B ) -> ( `' F " e ) e. ( S |`t dom F ) )
64 eqid 
 |-  ( ( `' F " e ) i^i ( `' F " dom H ) ) = ( ( `' F " e ) i^i ( `' F " dom H ) )
65 52 58 63 64 elrestd 
 |-  ( ( ph /\ e e. B ) -> ( ( `' F " e ) i^i ( `' F " dom H ) ) e. ( ( S |`t dom F ) |`t ( `' F " dom H ) ) )
66 inpreima 
 |-  ( Fun F -> ( `' F " ( e i^i dom H ) ) = ( ( `' F " e ) i^i ( `' F " dom H ) ) )
67 20 66 syl 
 |-  ( ph -> ( `' F " ( e i^i dom H ) ) = ( ( `' F " e ) i^i ( `' F " dom H ) ) )
68 67 adantr 
 |-  ( ( ph /\ e e. B ) -> ( `' F " ( e i^i dom H ) ) = ( ( `' F " e ) i^i ( `' F " dom H ) ) )
69 2 dmexd 
 |-  ( ph -> dom F e. _V )
70 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 ) ) )
71 1 8 69 70 syl3anc 
 |-  ( ph -> ( ( S |`t dom F ) |`t ( `' F " dom H ) ) = ( S |`t ( `' F " dom H ) ) )
72 71 eqcomd 
 |-  ( ph -> ( S |`t ( `' F " dom H ) ) = ( ( S |`t dom F ) |`t ( `' F " dom H ) ) )
73 72 adantr 
 |-  ( ( ph /\ e e. B ) -> ( S |`t ( `' F " dom H ) ) = ( ( S |`t dom F ) |`t ( `' F " dom H ) ) )
74 68 73 eleq12d 
 |-  ( ( ph /\ e e. B ) -> ( ( `' F " ( e i^i dom H ) ) e. ( S |`t ( `' F " dom H ) ) <-> ( ( `' F " e ) i^i ( `' F " dom H ) ) e. ( ( S |`t dom F ) |`t ( `' F " dom H ) ) ) )
75 65 74 mpbird 
 |-  ( ( ph /\ e e. B ) -> ( `' F " ( e i^i dom H ) ) e. ( S |`t ( `' F " dom H ) ) )
76 75 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 ) ) )
77 51 76 eqeltrd 
 |-  ( ( ph /\ e e. B /\ ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) e. ( S |`t ( `' F " dom H ) ) )
78 77 3exp 
 |-  ( ph -> ( e e. B -> ( ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) e. ( S |`t ( `' F " dom H ) ) ) ) )
79 78 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 ) ) ) ) )
80 79 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 ) ) ) )
81 49 80 mpd 
 |-  ( ( ph /\ a e. RR ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) e. ( S |`t ( `' F " dom H ) ) )
82 34 81 eqeltrd 
 |-  ( ( ph /\ a e. RR ) -> { x e. ( `' F " dom H ) | ( ( H o. F ) ` x ) < a } e. ( S |`t ( `' F " dom H ) ) )
83 6 1 11 23 82 issmfd 
 |-  ( ph -> ( H o. F ) e. ( SMblFn ` S ) )