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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 | |
|
2 | cncff | |
|
3 | 1 2 | syl | |
4 | simp2 | |
|
5 | fco | |
|
6 | 3 4 5 | syl2anc | |
7 | 4 | fdmd | |
8 | mbfdm | |
|
9 | 8 | 3ad2ant1 | |
10 | 7 9 | eqeltrrd | |
11 | mblss | |
|
12 | 10 11 | syl | |
13 | cnex | |
|
14 | reex | |
|
15 | elpm2r | |
|
16 | 13 14 15 | mpanl12 | |
17 | 6 12 16 | syl2anc | |
18 | coeq1 | |
|
19 | coass | |
|
20 | 18 19 | eqtrdi | |
21 | 20 | cnveqd | |
22 | 21 | imaeq1d | |
23 | 22 | eleq1d | |
24 | cnvco | |
|
25 | 24 | imaeq1i | |
26 | imaco | |
|
27 | 25 26 | eqtri | |
28 | simplll | |
|
29 | simpllr | |
|
30 | cncfrss | |
|
31 | 30 | adantl | |
32 | simpr | |
|
33 | ax-resscn | |
|
34 | eqid | |
|
35 | eqid | |
|
36 | 34 | tgioo2 | |
37 | 34 35 36 | cncfcn | |
38 | 31 33 37 | sylancl | |
39 | 32 38 | eleqtrd | |
40 | retopbas | |
|
41 | bastg | |
|
42 | 40 41 | ax-mp | |
43 | simplr | |
|
44 | 42 43 | sselid | |
45 | cnima | |
|
46 | 39 44 45 | syl2anc | |
47 | 34 35 | mbfimaopn2 | |
48 | 28 29 31 46 47 | syl31anc | |
49 | 27 48 | eqeltrid | |
50 | 49 | ralrimiva | |
51 | 50 | 3adantl3 | |
52 | recncf | |
|
53 | 52 | a1i | |
54 | 1 53 | cncfco | |
55 | 54 | adantr | |
56 | 23 51 55 | rspcdva | |
57 | coeq1 | |
|
58 | coass | |
|
59 | 57 58 | eqtrdi | |
60 | 59 | cnveqd | |
61 | 60 | imaeq1d | |
62 | 61 | eleq1d | |
63 | imcncf | |
|
64 | 63 | a1i | |
65 | 1 64 | cncfco | |
66 | 65 | adantr | |
67 | 62 51 66 | rspcdva | |
68 | 56 67 | jca | |
69 | 68 | ralrimiva | |
70 | ismbf1 | |
|
71 | 17 69 70 | sylanbrc | |