Metamath Proof Explorer

Theorem issmfgelem

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-closed 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 (iv) of Fremlin1 p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 issmfgelem.x 
 |-  F/ x ph
2 issmfgelem.a 
 |-  F/ a ph
3 issmfgelem.s 
 |-  ( ph -> S e. SAlg )
4 issmfgelem.d 
 |-  D = dom F
5 issmfgelem.i 
 |-  ( ph -> D C_ U. S )
6 issmfgelem.f 
 |-  ( ph -> F : D --> RR )
7 issmfgelem.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 9 rabeqdv 
 |-  ( ph -> { x e. D | a <_ ( F ` x ) } = { x e. U. ( S |`t D ) | a <_ ( F ` x ) } )
33 32 eleq1d 
 |-  ( ph -> ( { x e. D | a <_ ( F ` x ) } e. ( S |`t D ) <-> { x e. U. ( S |`t D ) | a <_ ( F ` x ) } e. ( S |`t D ) ) )
34 2 33 ralbid 
 |-  ( ph -> ( A. a e. RR { x e. D | a <_ ( F ` x ) } e. ( S |`t D ) <-> A. a e. RR { x e. U. ( S |`t D ) | a <_ ( F ` x ) } e. ( S |`t D ) ) )
35 7 34 mpbid 
 |-  ( ph -> A. a e. RR { x e. U. ( S |`t D ) | a <_ ( F ` x ) } e. ( S |`t D ) )
36 35 adantr 
 |-  ( ( ph /\ a e. RR ) -> A. a e. RR { x e. U. ( S |`t D ) | a <_ ( F ` x ) } e. ( S |`t D ) )
37 simpr 
 |-  ( ( ph /\ a e. RR ) -> a e. RR )
38 rspa 
 |-  ( ( A. a e. RR { x e. U. ( S |`t D ) | a <_ ( F ` x ) } e. ( S |`t D ) /\ a e. RR ) -> { x e. U. ( S |`t D ) | a <_ ( F ` x ) } e. ( S |`t D ) )
39 36 37 38 syl2anc 
 |-  ( ( ph /\ a e. RR ) -> { x e. U. ( S |`t D ) | a <_ ( F ` x ) } e. ( S |`t D ) )
40 39 adantlr 
 |-  ( ( ( ph /\ b e. RR ) /\ a e. RR ) -> { x e. U. ( S |`t D ) | a <_ ( F ` x ) } e. ( S |`t D ) )
41 simpr 
 |-  ( ( ph /\ b e. RR ) -> b e. RR )
42 13 15 23 24 31 40 41 salpreimagelt 
 |-  ( ( ph /\ b e. RR ) -> { x e. U. ( S |`t D ) | ( F ` x ) < b } e. ( S |`t D ) )
43 11 42 eqeltrd 
 |-  ( ( ph /\ b e. RR ) -> { x e. D | ( F ` x ) < b } e. ( S |`t D ) )
44 43 ralrimiva 
 |-  ( ph -> A. b e. RR { x e. D | ( F ` x ) < b } e. ( S |`t D ) )
45 5 6 44 3jca 
 |-  ( ph -> ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { x e. D | ( F ` x ) < b } e. ( S |`t D ) ) )
46 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 ) ) ) )
47 45 46 mpbird 
 |-  ( ph -> F e. ( SMblFn ` S ) )