Metamath Proof Explorer

Theorem issmflem

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

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

Proof

Step Hyp Ref Expression
1 issmflem.s 
 |-  ( ph -> S e. SAlg )
2 issmflem.d 
 |-  D = dom F
3 simpr 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> F e. ( SMblFn ` S ) )
4 df-smblfn 
 |-  SMblFn = ( s e. SAlg |-> { f e. ( RR ^pm U. s ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s |`t dom f ) } )
5 unieq 
 |-  ( s = S -> U. s = U. S )
6 5 oveq2d 
 |-  ( s = S -> ( RR ^pm U. s ) = ( RR ^pm U. S ) )
7 6 rabeqdv 
 |-  ( s = S -> { f e. ( RR ^pm U. s ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s |`t dom f ) } = { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s |`t dom f ) } )
8 oveq1 
 |-  ( s = S -> ( s |`t dom f ) = ( S |`t dom f ) )
9 8 eleq2d 
 |-  ( s = S -> ( ( `' f " ( -oo (,) a ) ) e. ( s |`t dom f ) <-> ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) ) )
10 9 ralbidv 
 |-  ( s = S -> ( A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s |`t dom f ) <-> A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) ) )
11 10 rabbidv 
 |-  ( s = S -> { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s |`t dom f ) } = { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) } )
12 7 11 eqtrd 
 |-  ( s = S -> { f e. ( RR ^pm U. s ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s |`t dom f ) } = { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) } )
13 ovex 
 |-  ( RR ^pm U. S ) e. _V
14 13 rabex 
 |-  { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) } e. _V
15 14 a1i 
 |-  ( ph -> { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) } e. _V )
16 4 12 1 15 fvmptd3 
 |-  ( ph -> ( SMblFn ` S ) = { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) } )
17 16 adantr 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> ( SMblFn ` S ) = { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) } )
18 3 17 eleqtrd 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> F e. { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) } )
19 elrabi 
 |-  ( F e. { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) } -> F e. ( RR ^pm U. S ) )
20 18 19 syl 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> F e. ( RR ^pm U. S ) )
21 elpmi2 
 |-  ( F e. ( RR ^pm U. S ) -> dom F C_ U. S )
22 2 21 eqsstrid 
 |-  ( F e. ( RR ^pm U. S ) -> D C_ U. S )
23 22 adantl 
 |-  ( ( ph /\ F e. ( RR ^pm U. S ) ) -> D C_ U. S )
24 20 23 syldan 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> D C_ U. S )
25 elpmi 
 |-  ( F e. ( RR ^pm U. S ) -> ( F : dom F --> RR /\ dom F C_ U. S ) )
26 20 25 syl 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> ( F : dom F --> RR /\ dom F C_ U. S ) )
27 26 simpld 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> F : dom F --> RR )
28 2 feq2i 
 |-  ( F : D --> RR <-> F : dom F --> RR )
29 28 a1i 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> ( F : D --> RR <-> F : dom F --> RR ) )
30 27 29 mpbird 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> F : D --> RR )
31 cnveq 
 |-  ( f = F -> `' f = `' F )
32 31 imaeq1d 
 |-  ( f = F -> ( `' f " ( -oo (,) a ) ) = ( `' F " ( -oo (,) a ) ) )
33 dmeq 
 |-  ( f = F -> dom f = dom F )
34 33 oveq2d 
 |-  ( f = F -> ( S |`t dom f ) = ( S |`t dom F ) )
35 32 34 eleq12d 
 |-  ( f = F -> ( ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) <-> ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) ) )
36 35 ralbidv 
 |-  ( f = F -> ( A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) <-> A. a e. RR ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) ) )
37 36 elrab 
 |-  ( F e. { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) } <-> ( F e. ( RR ^pm U. S ) /\ A. a e. RR ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) ) )
38 37 simprbi 
 |-  ( F e. { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) } -> A. a e. RR ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) )
39 18 38 syl 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> A. a e. RR ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) )
40 39 adantr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ a e. RR ) -> A. a e. RR ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) )
41 simpr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ a e. RR ) -> a e. RR )
42 rspa 
 |-  ( ( A. a e. RR ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) /\ a e. RR ) -> ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) )
43 40 41 42 syl2anc 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ a e. RR ) -> ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) )
44 30 adantr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ a e. RR ) -> F : D --> RR )
45 simpl 
 |-  ( ( F : D --> RR /\ a e. RR ) -> F : D --> RR )
46 simpr 
 |-  ( ( F : D --> RR /\ a e. RR ) -> a e. RR )
47 46 rexrd 
 |-  ( ( F : D --> RR /\ a e. RR ) -> a e. RR* )
48 45 47 preimaioomnf 
 |-  ( ( F : D --> RR /\ a e. RR ) -> ( `' F " ( -oo (,) a ) ) = { x e. D | ( F ` x ) < a } )
49 48 eqcomd 
 |-  ( ( F : D --> RR /\ a e. RR ) -> { x e. D | ( F ` x ) < a } = ( `' F " ( -oo (,) a ) ) )
50 44 41 49 syl2anc 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ a e. RR ) -> { x e. D | ( F ` x ) < a } = ( `' F " ( -oo (,) a ) ) )
51 2 oveq2i 
 |-  ( S |`t D ) = ( S |`t dom F )
52 51 a1i 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ a e. RR ) -> ( S |`t D ) = ( S |`t dom F ) )
53 50 52 eleq12d 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ a e. RR ) -> ( { x e. D | ( F ` x ) < a } e. ( S |`t D ) <-> ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) ) )
54 43 53 mpbird 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ a e. RR ) -> { x e. D | ( F ` x ) < a } e. ( S |`t D ) )
55 54 ralrimiva 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) )
56 24 30 55 3jca 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) )
57 56 ex 
 |-  ( ph -> ( F e. ( SMblFn ` S ) -> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) )
58 reex 
 |-  RR e. _V
59 58 a1i 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR ) ) -> RR e. _V )
60 1 uniexd 
 |-  ( ph -> U. S e. _V )
61 60 adantr 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR ) ) -> U. S e. _V )
62 simprr 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR ) ) -> F : D --> RR )
63 fssxp 
 |-  ( F : D --> RR -> F C_ ( D X. RR ) )
64 63 adantl 
 |-  ( ( D C_ U. S /\ F : D --> RR ) -> F C_ ( D X. RR ) )
65 xpss1 
 |-  ( D C_ U. S -> ( D X. RR ) C_ ( U. S X. RR ) )
66 65 adantr 
 |-  ( ( D C_ U. S /\ F : D --> RR ) -> ( D X. RR ) C_ ( U. S X. RR ) )
67 64 66 sstrd 
 |-  ( ( D C_ U. S /\ F : D --> RR ) -> F C_ ( U. S X. RR ) )
68 67 adantl 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR ) ) -> F C_ ( U. S X. RR ) )
69 dmss 
 |-  ( F C_ ( U. S X. RR ) -> dom F C_ dom ( U. S X. RR ) )
70 dmxpss 
 |-  dom ( U. S X. RR ) C_ U. S
71 70 a1i 
 |-  ( F C_ ( U. S X. RR ) -> dom ( U. S X. RR ) C_ U. S )
72 69 71 sstrd 
 |-  ( F C_ ( U. S X. RR ) -> dom F C_ U. S )
73 72 adantl 
 |-  ( ( ph /\ F C_ ( U. S X. RR ) ) -> dom F C_ U. S )
74 2 73 eqsstrid 
 |-  ( ( ph /\ F C_ ( U. S X. RR ) ) -> D C_ U. S )
75 68 74 syldan 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR ) ) -> D C_ U. S )
76 elpm2r 
 |-  ( ( ( RR e. _V /\ U. S e. _V ) /\ ( F : D --> RR /\ D C_ U. S ) ) -> F e. ( RR ^pm U. S ) )
77 59 61 62 75 76 syl22anc 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR ) ) -> F e. ( RR ^pm U. S ) )
78 77 3adantr3 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) -> F e. ( RR ^pm U. S ) )
79 2 a1i 
 |-  ( ( F : D --> RR /\ a e. RR ) -> D = dom F )
80 79 oveq2d 
 |-  ( ( F : D --> RR /\ a e. RR ) -> ( S |`t D ) = ( S |`t dom F ) )
81 49 80 eleq12d 
 |-  ( ( F : D --> RR /\ a e. RR ) -> ( { x e. D | ( F ` x ) < a } e. ( S |`t D ) <-> ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) ) )
82 81 ralbidva 
 |-  ( F : D --> RR -> ( A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) <-> A. a e. RR ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) ) )
83 82 biimpd 
 |-  ( F : D --> RR -> ( A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) -> A. a e. RR ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) ) )
84 83 imp 
 |-  ( ( F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) -> A. a e. RR ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) )
85 84 adantl 
 |-  ( ( ph /\ ( F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) -> A. a e. RR ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) )
86 85 3adantr1 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) -> A. a e. RR ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) )
87 78 86 jca 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) -> ( F e. ( RR ^pm U. S ) /\ A. a e. RR ( `' F " ( -oo (,) a ) ) e. ( S |`t dom F ) ) )
88 87 37 sylibr 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) -> F e. { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) } )
89 16 eqcomd 
 |-  ( ph -> { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) } = ( SMblFn ` S ) )
90 89 adantr 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) -> { f e. ( RR ^pm U. S ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( S |`t dom f ) } = ( SMblFn ` S ) )
91 88 90 eleqtrd 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) -> F e. ( SMblFn ` S ) )
92 91 ex 
 |-  ( ph -> ( ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) -> F e. ( SMblFn ` S ) ) )
93 57 92 impbid 
 |-  ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) )