Description: A continuous function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014) (Revised by Mario Carneiro, 26-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | cnmbf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cncff | |
|
2 | mblss | |
|
3 | cnex | |
|
4 | reex | |
|
5 | elpm2r | |
|
6 | 3 4 5 | mpanl12 | |
7 | 1 2 6 | syl2anr | |
8 | simpll | |
|
9 | simplr | |
|
10 | recncf | |
|
11 | 10 | a1i | |
12 | 9 11 | cncfco | |
13 | 2 | ad2antrr | |
14 | ax-resscn | |
|
15 | 13 14 | sstrdi | |
16 | eqid | |
|
17 | eqid | |
|
18 | 16 | tgioo2 | |
19 | 16 17 18 | cncfcn | |
20 | 15 14 19 | sylancl | |
21 | eqid | |
|
22 | 16 21 | rerest | |
23 | 13 22 | syl | |
24 | 23 | oveq1d | |
25 | 20 24 | eqtrd | |
26 | 12 25 | eleqtrd | |
27 | retopbas | |
|
28 | bastg | |
|
29 | 27 28 | ax-mp | |
30 | simpr | |
|
31 | 29 30 | sselid | |
32 | cnima | |
|
33 | 26 31 32 | syl2anc | |
34 | eqid | |
|
35 | 34 | subopnmbl | |
36 | 8 33 35 | syl2anc | |
37 | imcncf | |
|
38 | 37 | a1i | |
39 | 9 38 | cncfco | |
40 | 39 25 | eleqtrd | |
41 | cnima | |
|
42 | 40 31 41 | syl2anc | |
43 | 34 | subopnmbl | |
44 | 8 42 43 | syl2anc | |
45 | 36 44 | jca | |
46 | 45 | ralrimiva | |
47 | ismbf1 | |
|
48 | 7 46 47 | sylanbrc | |