Metamath Proof Explorer


Theorem decsmf

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

Ref Expression
Hypotheses decsmf.x x φ
decsmf.y y φ
decsmf.a φ A
decsmf.f φ F : A
decsmf.i φ x A y A x y F y F x
decsmf.j J = topGen ran .
decsmf.b B = SalGen J
Assertion decsmf φ F SMblFn B

Proof

Step Hyp Ref Expression
1 decsmf.x x φ
2 decsmf.y y φ
3 decsmf.a φ A
4 decsmf.f φ F : A
5 decsmf.i φ x A y A x y F y F x
6 decsmf.j J = topGen ran .
7 decsmf.b B = SalGen J
8 nfv a φ
9 retop topGen ran . Top
10 6 9 eqeltri J Top
11 10 a1i φ J Top
12 11 7 salgencld φ B SAlg
13 11 7 unisalgen2 φ B = J
14 6 unieqi J = topGen ran .
15 14 a1i φ J = topGen ran .
16 uniretop = topGen ran .
17 16 eqcomi topGen ran . =
18 17 a1i φ topGen ran . =
19 13 15 18 3eqtrrd φ = B
20 3 19 sseqtrd φ A B
21 nfv x a
22 1 21 nfan x φ a
23 nfv y a
24 2 23 nfan y φ a
25 3 adantr φ a A
26 4 frexr φ F : A *
27 26 adantr φ a F : A *
28 breq1 x = w x y w y
29 fveq2 x = w F x = F w
30 29 breq2d x = w F y F x F y F w
31 28 30 imbi12d x = w x y F y F x w y F y F w
32 breq2 y = z w y w z
33 fveq2 y = z F y = F z
34 33 breq1d y = z F y F w F z F w
35 32 34 imbi12d y = z w y F y F w w z F z F w
36 31 35 cbvral2vw x A y A x y F y F x w A z A w z F z F w
37 5 36 sylib φ w A z A w z F z F w
38 37 adantr φ a w A z A w z F z F w
39 38 36 sylibr φ a x A y A x y F y F x
40 rexr a a *
41 40 adantl φ a a *
42 eqid x A | a < F x = x A | a < F x
43 fveq2 w = x F w = F x
44 43 breq2d w = x a < F w a < F x
45 44 cbvrabv w A | a < F w = x A | a < F x
46 45 supeq1i sup w A | a < F w * < = sup x A | a < F x * <
47 eqid −∞ sup w A | a < F w * < = −∞ sup w A | a < F w * <
48 eqid −∞ sup w A | a < F w * < = −∞ sup w A | a < F w * <
49 22 24 25 27 39 6 7 41 42 46 47 48 decsmflem φ a b B x A | a < F x = b A
50 12 elexd φ B V
51 reex V
52 51 a1i φ V
53 52 3 ssexd φ A V
54 elrest B V A V x A | a < F x B 𝑡 A b B x A | a < F x = b A
55 50 53 54 syl2anc φ x A | a < F x B 𝑡 A b B x A | a < F x = b A
56 55 adantr φ a x A | a < F x B 𝑡 A b B x A | a < F x = b A
57 49 56 mpbird φ a x A | a < F x B 𝑡 A
58 8 12 20 4 57 issmfgtd φ F SMblFn B