Metamath Proof Explorer


Theorem decsmflem

Description: A nonincreasing function is Borel measurable. Proposition 121D (c) of Fremlin1 p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses decsmflem.x x φ
decsmflem.y y φ
decsmflem.a φ A
decsmflem.f φ F : A *
decsmflem.i φ x A y A x y F y F x
decsmflem.j J = topGen ran .
decsmflem.b B = SalGen J
decsmflem.r φ R *
decsmflem.l Y = x A | R < F x
decsmflem.c C = sup Y * <
decsmflem.d D = −∞ C
decsmflem.e E = −∞ C
Assertion decsmflem φ b B Y = b A

Proof

Step Hyp Ref Expression
1 decsmflem.x x φ
2 decsmflem.y y φ
3 decsmflem.a φ A
4 decsmflem.f φ F : A *
5 decsmflem.i φ x A y A x y F y F x
6 decsmflem.j J = topGen ran .
7 decsmflem.b B = SalGen J
8 decsmflem.r φ R *
9 decsmflem.l Y = x A | R < F x
10 decsmflem.c C = sup Y * <
11 decsmflem.d D = −∞ C
12 decsmflem.e E = −∞ C
13 mnfxr −∞ *
14 13 a1i φ C Y −∞ *
15 ssrab2 x A | R < F x A
16 9 15 eqsstri Y A
17 16 a1i φ Y A
18 17 3 sstrd φ Y
19 18 sselda φ C Y C
20 14 19 6 7 iocborel φ C Y −∞ C B
21 12 20 eqeltrid φ C Y E B
22 nfrab1 _ x x A | R < F x
23 9 22 nfcxfr _ x Y
24 nfcv _ x *
25 nfcv _ x <
26 23 24 25 nfsup _ x sup Y * <
27 10 26 nfcxfr _ x C
28 27 23 nfel x C Y
29 1 28 nfan x φ C Y
30 3 adantr φ C Y A
31 4 adantr φ C Y F : A *
32 5 adantr φ C Y x A y A x y F y F x
33 8 adantr φ C Y R *
34 simpr φ C Y C Y
35 29 30 31 32 33 9 10 34 12 pimdecfgtioc φ C Y Y = E A
36 ineq1 b = E b A = E A
37 36 rspceeqv E B Y = E A b B Y = b A
38 21 35 37 syl2anc φ C Y b B Y = b A
39 6 7 iooborel −∞ C B
40 11 39 eqeltri D B
41 40 a1i φ D B
42 41 adantr φ ¬ C Y D B
43 28 nfn x ¬ C Y
44 1 43 nfan x φ ¬ C Y
45 nfv y ¬ C Y
46 2 45 nfan y φ ¬ C Y
47 3 adantr φ ¬ C Y A
48 4 adantr φ ¬ C Y F : A *
49 5 adantr φ ¬ C Y x A y A x y F y F x
50 8 adantr φ ¬ C Y R *
51 simpr φ ¬ C Y ¬ C Y
52 44 46 47 48 49 50 9 10 51 11 pimdecfgtioo φ ¬ C Y Y = D A
53 ineq1 b = D b A = D A
54 53 rspceeqv D B Y = D A b B Y = b A
55 42 52 54 syl2anc φ ¬ C Y b B Y = b A
56 38 55 pm2.61dan φ b B Y = b A