Metamath Proof Explorer

Theorem issmflelem

Description: The predicate " F is a real-valued measurable function w.r.t. to the sigma-algebra S ". A function is measurable iff the preimages of all right-closed intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of F is required to be a subset of the underlying set of S . Definition 121C of Fremlin1 p. 36, and Proposition 121B (ii) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses issmflelem.x 
|- F/ x ph
issmflelem.a 
|- F/ a ph
issmflelem.s 
|- ( ph -> S e. SAlg )
issmflelem.d 
|- D = dom F
issmflelem.i 
|- ( ph -> D C_ U. S )
issmflelem.f 
|- ( ph -> F : D --> RR )
issmflelem.l 
|- ( ( ph /\ a e. RR ) -> { x e. D | ( F ` x ) <_ a } e. ( S |`t D ) )
Assertion issmflelem 
|- ( ph -> F e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 issmflelem.x 
 |-  F/ x ph
2 issmflelem.a 
 |-  F/ a ph
3 issmflelem.s 
 |-  ( ph -> S e. SAlg )
4 issmflelem.d 
 |-  D = dom F
5 issmflelem.i 
 |-  ( ph -> D C_ U. S )
6 issmflelem.f 
 |-  ( ph -> F : D --> RR )
7 issmflelem.l 
 |-  ( ( ph /\ a e. RR ) -> { x e. D | ( F ` x ) <_ a } e. ( S |`t D ) )
8 3 adantr 
 |-  ( ( ph /\ D C_ U. S ) -> S e. SAlg )
9 simpr 
 |-  ( ( ph /\ D C_ U. S ) -> D C_ U. S )
10 8 9 restuni4 
 |-  ( ( ph /\ D C_ U. S ) -> U. ( S |`t D ) = D )
11 10 eqcomd 
 |-  ( ( ph /\ D C_ U. S ) -> D = U. ( S |`t D ) )
12 5 11 mpdan 
 |-  ( ph -> D = U. ( S |`t D ) )
13 12 rabeqdv 
 |-  ( ph -> { x e. D | ( F ` x ) < b } = { x e. U. ( S |`t D ) | ( F ` x ) < b } )
14 13 adantr 
 |-  ( ( ph /\ b e. RR ) -> { x e. D | ( F ` x ) < b } = { x e. U. ( S |`t D ) | ( F ` x ) < b } )
15 nfv 
 |-  F/ x b e. RR
16 1 15 nfan 
 |-  F/ x ( ph /\ b e. RR )
17 nfv 
 |-  F/ a b e. RR
18 2 17 nfan 
 |-  F/ a ( ph /\ b e. RR )
19 3 uniexd 
 |-  ( ph -> U. S e. _V )
20 19 adantr 
 |-  ( ( ph /\ D C_ U. S ) -> U. S e. _V )
21 20 9 ssexd 
 |-  ( ( ph /\ D C_ U. S ) -> D e. _V )
22 eqid 
 |-  ( S |`t D ) = ( S |`t D )
23 8 21 22 subsalsal 
 |-  ( ( ph /\ D C_ U. S ) -> ( S |`t D ) e. SAlg )
24 5 23 mpdan 
 |-  ( ph -> ( S |`t D ) e. SAlg )
25 24 adantr 
 |-  ( ( ph /\ b e. RR ) -> ( S |`t D ) e. SAlg )
26 eqid 
 |-  U. ( S |`t D ) = U. ( S |`t D )
27 simpr 
 |-  ( ( ph /\ x e. U. ( S |`t D ) ) -> x e. U. ( S |`t D ) )
28 5 10 mpdan 
 |-  ( ph -> U. ( S |`t D ) = D )
29 28 adantr 
 |-  ( ( ph /\ x e. U. ( S |`t D ) ) -> U. ( S |`t D ) = D )
30 27 29 eleqtrd 
 |-  ( ( ph /\ x e. U. ( S |`t D ) ) -> x e. D )
31 6 ffvelcdmda 
 |-  ( ( ph /\ x e. D ) -> ( F ` x ) e. RR )
32 30 31 syldan 
 |-  ( ( ph /\ x e. U. ( S |`t D ) ) -> ( F ` x ) e. RR )
33 32 rexrd 
 |-  ( ( ph /\ x e. U. ( S |`t D ) ) -> ( F ` x ) e. RR* )
34 33 adantlr 
 |-  ( ( ( ph /\ b e. RR ) /\ x e. U. ( S |`t D ) ) -> ( F ` x ) e. RR* )
35 28 rabeqdv 
 |-  ( ph -> { x e. U. ( S |`t D ) | ( F ` x ) <_ a } = { x e. D | ( F ` x ) <_ a } )
36 35 adantr 
 |-  ( ( ph /\ a e. RR ) -> { x e. U. ( S |`t D ) | ( F ` x ) <_ a } = { x e. D | ( F ` x ) <_ a } )
37 36 7 eqeltrd 
 |-  ( ( ph /\ a e. RR ) -> { x e. U. ( S |`t D ) | ( F ` x ) <_ a } e. ( S |`t D ) )
38 37 adantlr 
 |-  ( ( ( ph /\ b e. RR ) /\ a e. RR ) -> { x e. U. ( S |`t D ) | ( F ` x ) <_ a } e. ( S |`t D ) )
39 simpr 
 |-  ( ( ph /\ b e. RR ) -> b e. RR )
40 16 18 25 26 34 38 39 salpreimalelt 
 |-  ( ( ph /\ b e. RR ) -> { x e. U. ( S |`t D ) | ( F ` x ) < b } e. ( S |`t D ) )
41 14 40 eqeltrd 
 |-  ( ( ph /\ b e. RR ) -> { x e. D | ( F ` x ) < b } e. ( S |`t D ) )
42 41 ralrimiva 
 |-  ( ph -> A. b e. RR { x e. D | ( F ` x ) < b } e. ( S |`t D ) )
43 5 6 42 3jca 
 |-  ( ph -> ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { x e. D | ( F ` x ) < b } e. ( S |`t D ) ) )
44 3 4 issmf 
 |-  ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { x e. D | ( F ` x ) < b } e. ( S |`t D ) ) ) )
45 43 44 mpbird 
 |-  ( ph -> F e. ( SMblFn ` S ) )