Metamath Proof Explorer


Theorem cncombf

Description: The composition of a continuous function with a measurable function is measurable. (More generally, G can be a Borel-measurable function, but notably the condition that G be only measurable is too weak, the usual counterexample taking G to be the Cantor function and F the indicator function of the G -image of a nonmeasurable set, which is a subset of the Cantor set and hence null and measurable.) (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Assertion cncombf FMblFnF:ABG:BcnGFMblFn

Proof

Step Hyp Ref Expression
1 simp3 FMblFnF:ABG:BcnG:Bcn
2 cncff G:BcnG:B
3 1 2 syl FMblFnF:ABG:BcnG:B
4 simp2 FMblFnF:ABG:BcnF:AB
5 fco G:BF:ABGF:A
6 3 4 5 syl2anc FMblFnF:ABG:BcnGF:A
7 4 fdmd FMblFnF:ABG:BcndomF=A
8 mbfdm FMblFndomFdomvol
9 8 3ad2ant1 FMblFnF:ABG:BcndomFdomvol
10 7 9 eqeltrrd FMblFnF:ABG:BcnAdomvol
11 mblss AdomvolA
12 10 11 syl FMblFnF:ABG:BcnA
13 cnex V
14 reex V
15 elpm2r VVGF:AAGF𝑝𝑚
16 13 14 15 mpanl12 GF:AAGF𝑝𝑚
17 6 12 16 syl2anc FMblFnF:ABG:BcnGF𝑝𝑚
18 coeq1 g=GgF=GF
19 coass GF=GF
20 18 19 eqtrdi g=GgF=GF
21 20 cnveqd g=GgF-1=GF-1
22 21 imaeq1d g=GgF-1x=GF-1x
23 22 eleq1d g=GgF-1xdomvolGF-1xdomvol
24 cnvco gF-1=F-1g-1
25 24 imaeq1i gF-1x=F-1g-1x
26 imaco F-1g-1x=F-1g-1x
27 25 26 eqtri gF-1x=F-1g-1x
28 simplll FMblFnF:ABxran.g:BcnFMblFn
29 simpllr FMblFnF:ABxran.g:BcnF:AB
30 cncfrss g:BcnB
31 30 adantl FMblFnF:ABxran.g:BcnB
32 simpr FMblFnF:ABxran.g:Bcng:Bcn
33 ax-resscn
34 eqid TopOpenfld=TopOpenfld
35 eqid TopOpenfld𝑡B=TopOpenfld𝑡B
36 34 tgioo2 topGenran.=TopOpenfld𝑡
37 34 35 36 cncfcn BBcn=TopOpenfld𝑡BCntopGenran.
38 31 33 37 sylancl FMblFnF:ABxran.g:BcnBcn=TopOpenfld𝑡BCntopGenran.
39 32 38 eleqtrd FMblFnF:ABxran.g:BcngTopOpenfld𝑡BCntopGenran.
40 retopbas ran.TopBases
41 bastg ran.TopBasesran.topGenran.
42 40 41 ax-mp ran.topGenran.
43 simplr FMblFnF:ABxran.g:Bcnxran.
44 42 43 sselid FMblFnF:ABxran.g:BcnxtopGenran.
45 cnima gTopOpenfld𝑡BCntopGenran.xtopGenran.g-1xTopOpenfld𝑡B
46 39 44 45 syl2anc FMblFnF:ABxran.g:Bcng-1xTopOpenfld𝑡B
47 34 35 mbfimaopn2 FMblFnF:ABBg-1xTopOpenfld𝑡BF-1g-1xdomvol
48 28 29 31 46 47 syl31anc FMblFnF:ABxran.g:BcnF-1g-1xdomvol
49 27 48 eqeltrid FMblFnF:ABxran.g:BcngF-1xdomvol
50 49 ralrimiva FMblFnF:ABxran.gBcngF-1xdomvol
51 50 3adantl3 FMblFnF:ABG:Bcnxran.gBcngF-1xdomvol
52 recncf :cn
53 52 a1i FMblFnF:ABG:Bcn:cn
54 1 53 cncfco FMblFnF:ABG:BcnG:Bcn
55 54 adantr FMblFnF:ABG:Bcnxran.G:Bcn
56 23 51 55 rspcdva FMblFnF:ABG:Bcnxran.GF-1xdomvol
57 coeq1 g=GgF=GF
58 coass GF=GF
59 57 58 eqtrdi g=GgF=GF
60 59 cnveqd g=GgF-1=GF-1
61 60 imaeq1d g=GgF-1x=GF-1x
62 61 eleq1d g=GgF-1xdomvolGF-1xdomvol
63 imcncf :cn
64 63 a1i FMblFnF:ABG:Bcn:cn
65 1 64 cncfco FMblFnF:ABG:BcnG:Bcn
66 65 adantr FMblFnF:ABG:Bcnxran.G:Bcn
67 62 51 66 rspcdva FMblFnF:ABG:Bcnxran.GF-1xdomvol
68 56 67 jca FMblFnF:ABG:Bcnxran.GF-1xdomvolGF-1xdomvol
69 68 ralrimiva FMblFnF:ABG:Bcnxran.GF-1xdomvolGF-1xdomvol
70 ismbf1 GFMblFnGF𝑝𝑚xran.GF-1xdomvolGF-1xdomvol
71 17 69 70 sylanbrc FMblFnF:ABG:BcnGFMblFn