Metamath Proof Explorer

Theorem incsmf

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

Ref Expression
Hypotheses incsmf.a 
|- ( ph -> A C_ RR )
incsmf.f 
|- ( ph -> F : A --> RR )
incsmf.i 
|- ( ph -> A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
incsmf.j 
|- J = ( topGen ` ran (,) )
incsmf.b 
|- B = ( SalGen ` J )
Assertion incsmf 
|- ( ph -> F e. ( SMblFn ` B ) )

Proof

Step Hyp Ref Expression
1 incsmf.a 
 |-  ( ph -> A C_ RR )
2 incsmf.f 
 |-  ( ph -> F : A --> RR )
3 incsmf.i 
 |-  ( ph -> A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
4 incsmf.j 
 |-  J = ( topGen ` ran (,) )
5 incsmf.b 
 |-  B = ( SalGen ` J )
6 nfv 
 |-  F/ a ph
7 retop 
 |-  ( topGen ` ran (,) ) e. Top
8 4 7 eqeltri 
 |-  J e. Top
9 8 a1i 
 |-  ( ph -> J e. Top )
10 9 5 salgencld 
 |-  ( ph -> B e. SAlg )
11 9 5 unisalgen2 
 |-  ( ph -> U. B = U. J )
12 4 unieqi 
 |-  U. J = U. ( topGen ` ran (,) )
13 12 a1i 
 |-  ( ph -> U. J = U. ( topGen ` ran (,) ) )
14 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
15 14 eqcomi 
 |-  U. ( topGen ` ran (,) ) = RR
16 15 a1i 
 |-  ( ph -> U. ( topGen ` ran (,) ) = RR )
17 11 13 16 3eqtrrd 
 |-  ( ph -> RR = U. B )
18 1 17 sseqtrd 
 |-  ( ph -> A C_ U. B )
19 nfv 
 |-  F/ w ( ph /\ a e. RR )
20 nfv 
 |-  F/ z ( ph /\ a e. RR )
21 1 adantr 
 |-  ( ( ph /\ a e. RR ) -> A C_ RR )
22 2 frexr 
 |-  ( ph -> F : A --> RR* )
23 22 adantr 
 |-  ( ( ph /\ a e. RR ) -> F : A --> RR* )
24 breq1 
 |-  ( x = w -> ( x <_ y <-> w <_ y ) )
25 fveq2 
 |-  ( x = w -> ( F ` x ) = ( F ` w ) )
26 25 breq1d 
 |-  ( x = w -> ( ( F ` x ) <_ ( F ` y ) <-> ( F ` w ) <_ ( F ` y ) ) )
27 24 26 imbi12d 
 |-  ( x = w -> ( ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) <-> ( w <_ y -> ( F ` w ) <_ ( F ` y ) ) ) )
28 breq2 
 |-  ( y = z -> ( w <_ y <-> w <_ z ) )
29 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
30 29 breq2d 
 |-  ( y = z -> ( ( F ` w ) <_ ( F ` y ) <-> ( F ` w ) <_ ( F ` z ) ) )
31 28 30 imbi12d 
 |-  ( y = z -> ( ( w <_ y -> ( F ` w ) <_ ( F ` y ) ) <-> ( w <_ z -> ( F ` w ) <_ ( F ` z ) ) ) )
32 27 31 cbvral2vw 
 |-  ( A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) <-> A. w e. A A. z e. A ( w <_ z -> ( F ` w ) <_ ( F ` z ) ) )
33 3 32 sylib 
 |-  ( ph -> A. w e. A A. z e. A ( w <_ z -> ( F ` w ) <_ ( F ` z ) ) )
34 33 adantr 
 |-  ( ( ph /\ a e. RR ) -> A. w e. A A. z e. A ( w <_ z -> ( F ` w ) <_ ( F ` z ) ) )
35 rexr 
 |-  ( a e. RR -> a e. RR* )
36 35 adantl 
 |-  ( ( ph /\ a e. RR ) -> a e. RR* )
37 25 breq1d 
 |-  ( x = w -> ( ( F ` x ) < a <-> ( F ` w ) < a ) )
38 37 cbvrabv 
 |-  { x e. A | ( F ` x ) < a } = { w e. A | ( F ` w ) < a }
39 eqid 
 |-  sup ( { x e. A | ( F ` x ) < a } , RR* , < ) = sup ( { x e. A | ( F ` x ) < a } , RR* , < )
40 eqid 
 |-  ( -oo (,) sup ( { x e. A | ( F ` x ) < a } , RR* , < ) ) = ( -oo (,) sup ( { x e. A | ( F ` x ) < a } , RR* , < ) )
41 eqid 
 |-  ( -oo (,] sup ( { x e. A | ( F ` x ) < a } , RR* , < ) ) = ( -oo (,] sup ( { x e. A | ( F ` x ) < a } , RR* , < ) )
42 19 20 21 23 34 4 5 36 38 39 40 41 incsmflem 
 |-  ( ( ph /\ a e. RR ) -> E. b e. B { x e. A | ( F ` x ) < a } = ( b i^i A ) )
43 reex 
 |-  RR e. _V
44 43 a1i 
 |-  ( ph -> RR e. _V )
45 44 1 ssexd 
 |-  ( ph -> A e. _V )
46 elrest 
 |-  ( ( B e. SAlg /\ A e. _V ) -> ( { x e. A | ( F ` x ) < a } e. ( B |`t A ) <-> E. b e. B { x e. A | ( F ` x ) < a } = ( b i^i A ) ) )
47 10 45 46 syl2anc 
 |-  ( ph -> ( { x e. A | ( F ` x ) < a } e. ( B |`t A ) <-> E. b e. B { x e. A | ( F ` x ) < a } = ( b i^i A ) ) )
48 47 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( { x e. A | ( F ` x ) < a } e. ( B |`t A ) <-> E. b e. B { x e. A | ( F ` x ) < a } = ( b i^i A ) ) )
49 42 48 mpbird 
 |-  ( ( ph /\ a e. RR ) -> { x e. A | ( F ` x ) < a } e. ( B |`t A ) )
50 6 10 18 2 49 issmfd 
 |-  ( ph -> F e. ( SMblFn ` B ) )