Description: Deduction to prove measurability of a real function. The third hypothesis is not necessary, but the proof of this requires countable choice, so we derive this separately as ismbf3d . (Contributed by Mario Carneiro, 18-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ismbfd.1 | |
|
ismbfd.2 | |
||
ismbfd.3 | |
||
Assertion | ismbfd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismbfd.1 | |
|
2 | ismbfd.2 | |
|
3 | ismbfd.3 | |
|
4 | ioof | |
|
5 | ffn | |
|
6 | ovelrn | |
|
7 | 4 5 6 | mp2b | |
8 | simprl | |
|
9 | pnfxr | |
|
10 | 9 | a1i | |
11 | mnfxr | |
|
12 | 11 | a1i | |
13 | simprr | |
|
14 | iooin | |
|
15 | 8 10 12 13 14 | syl22anc | |
16 | ifcl | |
|
17 | 11 8 16 | sylancr | |
18 | mnfle | |
|
19 | xrleid | |
|
20 | breq1 | |
|
21 | breq1 | |
|
22 | 20 21 | ifboth | |
23 | 18 19 22 | syl2anc | |
24 | 23 | ad2antrl | |
25 | xrmax1 | |
|
26 | 8 11 25 | sylancl | |
27 | 17 8 24 26 | xrletrid | |
28 | ifcl | |
|
29 | 9 13 28 | sylancr | |
30 | xrmin2 | |
|
31 | 9 13 30 | sylancr | |
32 | pnfge | |
|
33 | xrleid | |
|
34 | breq2 | |
|
35 | breq2 | |
|
36 | 34 35 | ifboth | |
37 | 32 33 36 | syl2anc | |
38 | 37 | ad2antll | |
39 | 29 13 31 38 | xrletrid | |
40 | 27 39 | oveq12d | |
41 | 15 40 | eqtrd | |
42 | 41 | imaeq2d | |
43 | 1 | adantr | |
44 | 43 | ffund | |
45 | inpreima | |
|
46 | 44 45 | syl | |
47 | 42 46 | eqtr3d | |
48 | 2 | adantrr | |
49 | 3 | ralrimiva | |
50 | oveq2 | |
|
51 | 50 | imaeq2d | |
52 | 51 | eleq1d | |
53 | 52 | rspccva | |
54 | 49 53 | sylan | |
55 | 54 | adantrl | |
56 | inmbl | |
|
57 | 48 55 56 | syl2anc | |
58 | 47 57 | eqeltrd | |
59 | imaeq2 | |
|
60 | 59 | eleq1d | |
61 | 58 60 | syl5ibrcom | |
62 | 61 | rexlimdvva | |
63 | 7 62 | syl5bi | |
64 | 63 | ralrimiv | |
65 | ismbf | |
|
66 | 1 65 | syl | |
67 | 64 66 | mpbird | |