Metamath Proof Explorer


Theorem incsmflem

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 xφ
incsmflem.y yφ
incsmflem.a φA
incsmflem.f φF:A*
incsmflem.i φxAyAxyFxFy
incsmflem.j J=topGenran.
incsmflem.b B=SalGenJ
incsmflem.r φR*
incsmflem.l Y=xA|Fx<R
incsmflem.c C=supY*<
incsmflem.d D=−∞C
incsmflem.e E=−∞C
Assertion incsmflem φbBY=bA

Proof

Step Hyp Ref Expression
1 incsmflem.x xφ
2 incsmflem.y yφ
3 incsmflem.a φA
4 incsmflem.f φF:A*
5 incsmflem.i φxAyAxyFxFy
6 incsmflem.j J=topGenran.
7 incsmflem.b B=SalGenJ
8 incsmflem.r φR*
9 incsmflem.l Y=xA|Fx<R
10 incsmflem.c C=supY*<
11 incsmflem.d D=−∞C
12 incsmflem.e E=−∞C
13 mnfxr −∞*
14 13 a1i φCY−∞*
15 ssrab2 xA|Fx<RA
16 9 15 eqsstri YA
17 16 a1i φYA
18 17 3 sstrd φY
19 18 sselda φCYC
20 14 19 6 7 iocborel φCY−∞CB
21 12 20 eqeltrid φCYEB
22 nfcv _xC
23 nfrab1 _xxA|Fx<R
24 9 23 nfcxfr _xY
25 22 24 nfel xCY
26 1 25 nfan xφCY
27 nfv yCY
28 2 27 nfan yφCY
29 3 adantr φCYA
30 4 adantr φCYF:A*
31 5 adantr φCYxAyAxyFxFy
32 8 adantr φCYR*
33 simpr φCYCY
34 26 28 29 30 31 32 9 10 33 12 pimincfltioc φCYY=EA
35 ineq1 b=EbA=EA
36 35 rspceeqv EBY=EAbBY=bA
37 21 34 36 syl2anc φCYbBY=bA
38 6 7 iooborel −∞CB
39 11 38 eqeltri DB
40 39 a1i φDB
41 40 adantr φ¬CYDB
42 25 nfn x¬CY
43 1 42 nfan xφ¬CY
44 nfv y¬CY
45 2 44 nfan yφ¬CY
46 3 adantr φ¬CYA
47 4 adantr φ¬CYF:A*
48 5 adantr φ¬CYxAyAxyFxFy
49 8 adantr φ¬CYR*
50 simpr φ¬CY¬CY
51 43 45 46 47 48 49 9 10 50 11 pimincfltioo φ¬CYY=DA
52 ineq1 b=DbA=DA
53 52 rspceeqv DBY=DAbBY=bA
54 41 51 53 syl2anc φ¬CYbBY=bA
55 37 54 pm2.61dan φbBY=bA