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 | |
|
issmfgelem.a | |
||
issmfgelem.s | |
||
issmfgelem.d | |
||
issmfgelem.i | |
||
issmfgelem.f | |
||
issmfgelem.p | |
||
Assertion | issmfgelem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | issmfgelem.x | |
|
2 | issmfgelem.a | |
|
3 | issmfgelem.s | |
|
4 | issmfgelem.d | |
|
5 | issmfgelem.i | |
|
6 | issmfgelem.f | |
|
7 | issmfgelem.p | |
|
8 | 3 5 | restuni4 | |
9 | 8 | eqcomd | |
10 | 9 | rabeqdv | |
11 | 10 | adantr | |
12 | nfv | |
|
13 | 1 12 | nfan | |
14 | nfv | |
|
15 | 2 14 | nfan | |
16 | 3 | uniexd | |
17 | 16 | adantr | |
18 | simpr | |
|
19 | 17 18 | ssexd | |
20 | 5 19 | mpdan | |
21 | eqid | |
|
22 | 3 20 21 | subsalsal | |
23 | 22 | adantr | |
24 | eqid | |
|
25 | 6 | adantr | |
26 | simpr | |
|
27 | 8 | adantr | |
28 | 26 27 | eleqtrd | |
29 | 25 28 | ffvelrnd | |
30 | 29 | rexrd | |
31 | 30 | adantlr | |
32 | 9 | rabeqdv | |
33 | 32 | eleq1d | |
34 | 2 33 | ralbid | |
35 | 7 34 | mpbid | |
36 | 35 | adantr | |
37 | simpr | |
|
38 | rspa | |
|
39 | 36 37 38 | syl2anc | |
40 | 39 | adantlr | |
41 | simpr | |
|
42 | 13 15 23 24 31 40 41 | salpreimagelt | |
43 | 11 42 | eqeltrd | |
44 | 43 | ralrimiva | |
45 | 5 6 44 | 3jca | |
46 | 3 4 | issmf | |
47 | 45 46 | mpbird | |