Metamath Proof Explorer


Theorem mbfres

Description: The restriction of a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion mbfres FMblFnAdomvolFAMblFn

Proof

Step Hyp Ref Expression
1 ref :
2 simpr FMblFnAdomvolAdomvol
3 ismbf1 FMblFnF𝑝𝑚xran.F-1xdomvolF-1xdomvol
4 3 simplbi FMblFnF𝑝𝑚
5 4 adantr FMblFnAdomvolF𝑝𝑚
6 pmresg AdomvolF𝑝𝑚FA𝑝𝑚A
7 2 5 6 syl2anc FMblFnAdomvolFA𝑝𝑚A
8 cnex V
9 elpm2g VAdomvolFA𝑝𝑚AFA:domFAdomFAA
10 8 2 9 sylancr FMblFnAdomvolFA𝑝𝑚AFA:domFAdomFAA
11 7 10 mpbid FMblFnAdomvolFA:domFAdomFAA
12 11 simpld FMblFnAdomvolFA:domFA
13 fco :FA:domFAFA:domFA
14 1 12 13 sylancr FMblFnAdomvolFA:domFA
15 dmres domFA=AdomF
16 id AdomvolAdomvol
17 mbfdm FMblFndomFdomvol
18 inmbl AdomvoldomFdomvolAdomFdomvol
19 16 17 18 syl2anr FMblFnAdomvolAdomFdomvol
20 15 19 eqeltrid FMblFnAdomvoldomFAdomvol
21 resco FA=FA
22 21 cnveqi FA-1=FA-1
23 22 imaeq1i FA-1x+∞=FA-1x+∞
24 cnvresima FA-1x+∞=F-1x+∞A
25 23 24 eqtr3i FA-1x+∞=F-1x+∞A
26 mbff FMblFnF:domF
27 ismbfcn F:domFFMblFnFMblFnFMblFn
28 26 27 syl FMblFnFMblFnFMblFnFMblFn
29 28 ibi FMblFnFMblFnFMblFn
30 29 simpld FMblFnFMblFn
31 fco :F:domFF:domF
32 1 26 31 sylancr FMblFnF:domF
33 mbfima FMblFnF:domFF-1x+∞domvol
34 30 32 33 syl2anc FMblFnF-1x+∞domvol
35 inmbl F-1x+∞domvolAdomvolF-1x+∞Adomvol
36 34 35 sylan FMblFnAdomvolF-1x+∞Adomvol
37 25 36 eqeltrid FMblFnAdomvolFA-1x+∞domvol
38 37 adantr FMblFnAdomvolxFA-1x+∞domvol
39 22 imaeq1i FA-1−∞x=FA-1−∞x
40 cnvresima FA-1−∞x=F-1−∞xA
41 39 40 eqtr3i FA-1−∞x=F-1−∞xA
42 mbfima FMblFnF:domFF-1−∞xdomvol
43 30 32 42 syl2anc FMblFnF-1−∞xdomvol
44 inmbl F-1−∞xdomvolAdomvolF-1−∞xAdomvol
45 43 44 sylan FMblFnAdomvolF-1−∞xAdomvol
46 41 45 eqeltrid FMblFnAdomvolFA-1−∞xdomvol
47 46 adantr FMblFnAdomvolxFA-1−∞xdomvol
48 14 20 38 47 ismbf2d FMblFnAdomvolFAMblFn
49 imf :
50 fco :FA:domFAFA:domFA
51 49 12 50 sylancr FMblFnAdomvolFA:domFA
52 resco FA=FA
53 52 cnveqi FA-1=FA-1
54 53 imaeq1i FA-1x+∞=FA-1x+∞
55 cnvresima FA-1x+∞=F-1x+∞A
56 54 55 eqtr3i FA-1x+∞=F-1x+∞A
57 29 simprd FMblFnFMblFn
58 fco :F:domFF:domF
59 49 26 58 sylancr FMblFnF:domF
60 mbfima FMblFnF:domFF-1x+∞domvol
61 57 59 60 syl2anc FMblFnF-1x+∞domvol
62 inmbl F-1x+∞domvolAdomvolF-1x+∞Adomvol
63 61 62 sylan FMblFnAdomvolF-1x+∞Adomvol
64 56 63 eqeltrid FMblFnAdomvolFA-1x+∞domvol
65 64 adantr FMblFnAdomvolxFA-1x+∞domvol
66 53 imaeq1i FA-1−∞x=FA-1−∞x
67 cnvresima FA-1−∞x=F-1−∞xA
68 66 67 eqtr3i FA-1−∞x=F-1−∞xA
69 mbfima FMblFnF:domFF-1−∞xdomvol
70 57 59 69 syl2anc FMblFnF-1−∞xdomvol
71 inmbl F-1−∞xdomvolAdomvolF-1−∞xAdomvol
72 70 71 sylan FMblFnAdomvolF-1−∞xAdomvol
73 68 72 eqeltrid FMblFnAdomvolFA-1−∞xdomvol
74 73 adantr FMblFnAdomvolxFA-1−∞xdomvol
75 51 20 65 74 ismbf2d FMblFnAdomvolFAMblFn
76 ismbfcn FA:domFAFAMblFnFAMblFnFAMblFn
77 12 76 syl FMblFnAdomvolFAMblFnFAMblFnFAMblFn
78 48 75 77 mpbir2and FMblFnAdomvolFAMblFn