Metamath Proof Explorer


Theorem cnmbf

Description: A continuous function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014) (Revised by Mario Carneiro, 26-Mar-2015)

Ref Expression
Assertion cnmbf AdomvolF:AcnFMblFn

Proof

Step Hyp Ref Expression
1 cncff F:AcnF:A
2 mblss AdomvolA
3 cnex V
4 reex V
5 elpm2r VVF:AAF𝑝𝑚
6 3 4 5 mpanl12 F:AAF𝑝𝑚
7 1 2 6 syl2anr AdomvolF:AcnF𝑝𝑚
8 simpll AdomvolF:Acnxran.Adomvol
9 simplr AdomvolF:Acnxran.F:Acn
10 recncf :cn
11 10 a1i AdomvolF:Acnxran.:cn
12 9 11 cncfco AdomvolF:Acnxran.F:Acn
13 2 ad2antrr AdomvolF:Acnxran.A
14 ax-resscn
15 13 14 sstrdi AdomvolF:Acnxran.A
16 eqid TopOpenfld=TopOpenfld
17 eqid TopOpenfld𝑡A=TopOpenfld𝑡A
18 16 tgioo2 topGenran.=TopOpenfld𝑡
19 16 17 18 cncfcn AAcn=TopOpenfld𝑡ACntopGenran.
20 15 14 19 sylancl AdomvolF:Acnxran.Acn=TopOpenfld𝑡ACntopGenran.
21 eqid topGenran.=topGenran.
22 16 21 rerest ATopOpenfld𝑡A=topGenran.𝑡A
23 13 22 syl AdomvolF:Acnxran.TopOpenfld𝑡A=topGenran.𝑡A
24 23 oveq1d AdomvolF:Acnxran.TopOpenfld𝑡ACntopGenran.=topGenran.𝑡ACntopGenran.
25 20 24 eqtrd AdomvolF:Acnxran.Acn=topGenran.𝑡ACntopGenran.
26 12 25 eleqtrd AdomvolF:Acnxran.FtopGenran.𝑡ACntopGenran.
27 retopbas ran.TopBases
28 bastg ran.TopBasesran.topGenran.
29 27 28 ax-mp ran.topGenran.
30 simpr AdomvolF:Acnxran.xran.
31 29 30 sselid AdomvolF:Acnxran.xtopGenran.
32 cnima FtopGenran.𝑡ACntopGenran.xtopGenran.F-1xtopGenran.𝑡A
33 26 31 32 syl2anc AdomvolF:Acnxran.F-1xtopGenran.𝑡A
34 eqid topGenran.𝑡A=topGenran.𝑡A
35 34 subopnmbl AdomvolF-1xtopGenran.𝑡AF-1xdomvol
36 8 33 35 syl2anc AdomvolF:Acnxran.F-1xdomvol
37 imcncf :cn
38 37 a1i AdomvolF:Acnxran.:cn
39 9 38 cncfco AdomvolF:Acnxran.F:Acn
40 39 25 eleqtrd AdomvolF:Acnxran.FtopGenran.𝑡ACntopGenran.
41 cnima FtopGenran.𝑡ACntopGenran.xtopGenran.F-1xtopGenran.𝑡A
42 40 31 41 syl2anc AdomvolF:Acnxran.F-1xtopGenran.𝑡A
43 34 subopnmbl AdomvolF-1xtopGenran.𝑡AF-1xdomvol
44 8 42 43 syl2anc AdomvolF:Acnxran.F-1xdomvol
45 36 44 jca AdomvolF:Acnxran.F-1xdomvolF-1xdomvol
46 45 ralrimiva AdomvolF:Acnxran.F-1xdomvolF-1xdomvol
47 ismbf1 FMblFnF𝑝𝑚xran.F-1xdomvolF-1xdomvol
48 7 46 47 sylanbrc AdomvolF:AcnFMblFn