Description: A nondecreasing function is Borel measurable. Proposition 121D (c) of Fremlin1 p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | incsmflem.x | |
|
incsmflem.y | |
||
incsmflem.a | |
||
incsmflem.f | |
||
incsmflem.i | |
||
incsmflem.j | |
||
incsmflem.b | |
||
incsmflem.r | |
||
incsmflem.l | |
||
incsmflem.c | |
||
incsmflem.d | |
||
incsmflem.e | |
||
Assertion | incsmflem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | incsmflem.x | |
|
2 | incsmflem.y | |
|
3 | incsmflem.a | |
|
4 | incsmflem.f | |
|
5 | incsmflem.i | |
|
6 | incsmflem.j | |
|
7 | incsmflem.b | |
|
8 | incsmflem.r | |
|
9 | incsmflem.l | |
|
10 | incsmflem.c | |
|
11 | incsmflem.d | |
|
12 | incsmflem.e | |
|
13 | mnfxr | |
|
14 | 13 | a1i | |
15 | ssrab2 | |
|
16 | 9 15 | eqsstri | |
17 | 16 | a1i | |
18 | 17 3 | sstrd | |
19 | 18 | sselda | |
20 | 14 19 6 7 | iocborel | |
21 | 12 20 | eqeltrid | |
22 | nfcv | |
|
23 | nfrab1 | |
|
24 | 9 23 | nfcxfr | |
25 | 22 24 | nfel | |
26 | 1 25 | nfan | |
27 | nfv | |
|
28 | 2 27 | nfan | |
29 | 3 | adantr | |
30 | 4 | adantr | |
31 | 5 | adantr | |
32 | 8 | adantr | |
33 | simpr | |
|
34 | 26 28 29 30 31 32 9 10 33 12 | pimincfltioc | |
35 | ineq1 | |
|
36 | 35 | rspceeqv | |
37 | 21 34 36 | syl2anc | |
38 | 6 7 | iooborel | |
39 | 11 38 | eqeltri | |
40 | 39 | a1i | |
41 | 40 | adantr | |
42 | 25 | nfn | |
43 | 1 42 | nfan | |
44 | nfv | |
|
45 | 2 44 | nfan | |
46 | 3 | adantr | |
47 | 4 | adantr | |
48 | 5 | adantr | |
49 | 8 | adantr | |
50 | simpr | |
|
51 | 43 45 46 47 48 49 9 10 50 11 | pimincfltioo | |
52 | ineq1 | |
|
53 | 52 | rspceeqv | |
54 | 41 51 53 | syl2anc | |
55 | 37 54 | pm2.61dan | |