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 | |
|
issmfgtlem.a | |
||
issmfgtlem.s | |
||
issmfgtlem.d | |
||
issmfgtlem.i | |
||
issmfgtlem.f | |
||
issmfgtlem.p | |
||
Assertion | issmfgtlem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | issmfgtlem.x | |
|
2 | issmfgtlem.a | |
|
3 | issmfgtlem.s | |
|
4 | issmfgtlem.d | |
|
5 | issmfgtlem.i | |
|
6 | issmfgtlem.f | |
|
7 | issmfgtlem.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 | 8 | rabeqdv | |
33 | 32 | adantr | |
34 | 7 | r19.21bi | |
35 | 33 34 | eqeltrd | |
36 | 35 | adantlr | |
37 | simpr | |
|
38 | 13 15 23 24 31 36 37 | salpreimagtlt | |
39 | 11 38 | eqeltrd | |
40 | 39 | ralrimiva | |
41 | 5 6 40 | 3jca | |
42 | 3 4 | issmf | |
43 | 41 42 | mpbird | |