Description: If all the preimages of right-closed, unbounded below intervals, belong to a sigma-algebra, then all the preimages of left-open, unbounded above intervals, belong to the sigma-algebra. (ii) implies (iii) in Proposition 121B of Fremlin1 p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | salpreimalegt.x | |
|
salpreimalegt.a | |
||
salpreimalegt.s | |
||
salpreimalegt.u | |
||
salpreimalegt.b | |
||
salpreimalegt.p | |
||
salpreimalegt.c | |
||
Assertion | salpreimalegt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | salpreimalegt.x | |
|
2 | salpreimalegt.a | |
|
3 | salpreimalegt.s | |
|
4 | salpreimalegt.u | |
|
5 | salpreimalegt.b | |
|
6 | salpreimalegt.p | |
|
7 | salpreimalegt.c | |
|
8 | 4 | eqcomi | |
9 | 8 | a1i | |
10 | 9 | difeq1d | |
11 | 7 | rexrd | |
12 | 1 5 11 | preimalegt | |
13 | 10 12 | eqtr2d | |
14 | 7 | ancli | |
15 | nfv | |
|
16 | 2 15 | nfan | |
17 | nfv | |
|
18 | 16 17 | nfim | |
19 | eleq1 | |
|
20 | 19 | anbi2d | |
21 | breq2 | |
|
22 | 21 | rabbidv | |
23 | 22 | eleq1d | |
24 | 20 23 | imbi12d | |
25 | 18 24 6 | vtoclg1f | |
26 | 7 14 25 | sylc | |
27 | 3 26 | saldifcld | |
28 | 13 27 | eqeltrd | |