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 
|- F/ x ph
decsmf.y 
|- F/ y ph
decsmf.a 
|- ( ph -> A C_ RR )
decsmf.f 
|- ( ph -> F : A --> RR )
decsmf.i 
|- ( ph -> A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) )
decsmf.j 
|- J = ( topGen ` ran (,) )
decsmf.b 
|- B = ( SalGen ` J )
Assertion decsmf 
|- ( ph -> F e. ( SMblFn ` B ) )

Proof

Step Hyp Ref Expression
1 decsmf.x 
 |-  F/ x ph
2 decsmf.y 
 |-  F/ y ph
3 decsmf.a 
 |-  ( ph -> A C_ RR )
4 decsmf.f 
 |-  ( ph -> F : A --> RR )
5 decsmf.i 
 |-  ( ph -> A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) )
6 decsmf.j 
 |-  J = ( topGen ` ran (,) )
7 decsmf.b 
 |-  B = ( SalGen ` J )
8 nfv 
 |-  F/ a ph
9 retop 
 |-  ( topGen ` ran (,) ) e. Top
10 6 9 eqeltri 
 |-  J e. Top
11 10 a1i 
 |-  ( ph -> J e. Top )
12 11 7 salgencld 
 |-  ( ph -> B e. SAlg )
13 11 7 unisalgen2 
 |-  ( ph -> U. B = U. J )
14 6 unieqi 
 |-  U. J = U. ( topGen ` ran (,) )
15 14 a1i 
 |-  ( ph -> U. J = U. ( topGen ` ran (,) ) )
16 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
17 16 eqcomi 
 |-  U. ( topGen ` ran (,) ) = RR
18 17 a1i 
 |-  ( ph -> U. ( topGen ` ran (,) ) = RR )
19 13 15 18 3eqtrrd 
 |-  ( ph -> RR = U. B )
20 3 19 sseqtrd 
 |-  ( ph -> A C_ U. B )
21 nfv 
 |-  F/ x a e. RR
22 1 21 nfan 
 |-  F/ x ( ph /\ a e. RR )
23 nfv 
 |-  F/ y a e. RR
24 2 23 nfan 
 |-  F/ y ( ph /\ a e. RR )
25 3 adantr 
 |-  ( ( ph /\ a e. RR ) -> A C_ RR )
26 4 frexr 
 |-  ( ph -> F : A --> RR* )
27 26 adantr 
 |-  ( ( ph /\ a e. RR ) -> F : A --> RR* )
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 
 |-  ( A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) <-> A. w e. A A. z e. A ( w <_ z -> ( F ` z ) <_ ( F ` w ) ) )
37 5 36 sylib 
 |-  ( ph -> A. w e. A A. z e. A ( w <_ z -> ( F ` z ) <_ ( F ` w ) ) )
38 37 adantr 
 |-  ( ( ph /\ a e. RR ) -> A. w e. A A. z e. A ( w <_ z -> ( F ` z ) <_ ( F ` w ) ) )
39 38 36 sylibr 
 |-  ( ( ph /\ a e. RR ) -> A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) )
40 rexr 
 |-  ( a e. RR -> a e. RR* )
41 40 adantl 
 |-  ( ( ph /\ a e. RR ) -> a e. RR* )
42 eqid 
 |-  { x e. A | a < ( F ` x ) } = { x e. 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 e. A | a < ( F ` w ) } = { x e. A | a < ( F ` x ) }
46 45 supeq1i 
 |-  sup ( { w e. A | a < ( F ` w ) } , RR* , < ) = sup ( { x e. A | a < ( F ` x ) } , RR* , < )
47 eqid 
 |-  ( -oo (,) sup ( { w e. A | a < ( F ` w ) } , RR* , < ) ) = ( -oo (,) sup ( { w e. A | a < ( F ` w ) } , RR* , < ) )
48 eqid 
 |-  ( -oo (,] sup ( { w e. A | a < ( F ` w ) } , RR* , < ) ) = ( -oo (,] sup ( { w e. A | a < ( F ` w ) } , RR* , < ) )
49 22 24 25 27 39 6 7 41 42 46 47 48 decsmflem 
 |-  ( ( ph /\ a e. RR ) -> E. b e. B { x e. A | a < ( F ` x ) } = ( b i^i A ) )
50 12 elexd 
 |-  ( ph -> B e. _V )
51 reex 
 |-  RR e. _V
52 51 a1i 
 |-  ( ph -> RR e. _V )
53 52 3 ssexd 
 |-  ( ph -> A e. _V )
54 elrest 
 |-  ( ( B e. _V /\ A e. _V ) -> ( { x e. A | a < ( F ` x ) } e. ( B |`t A ) <-> E. b e. B { x e. A | a < ( F ` x ) } = ( b i^i A ) ) )
55 50 53 54 syl2anc 
 |-  ( ph -> ( { x e. A | a < ( F ` x ) } e. ( B |`t A ) <-> E. b e. B { x e. A | a < ( F ` x ) } = ( b i^i A ) ) )
56 55 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( { x e. A | a < ( F ` x ) } e. ( B |`t A ) <-> E. b e. B { x e. A | a < ( F ` x ) } = ( b i^i A ) ) )
57 49 56 mpbird 
 |-  ( ( ph /\ a e. RR ) -> { x e. A | a < ( F ` x ) } e. ( B |`t A ) )
58 8 12 20 4 57 issmfgtd 
 |-  ( ph -> F e. ( SMblFn ` B ) )