Metamath Proof Explorer

Theorem issmfgtlem

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 left-open intervals unbounded above 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 (iii) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

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