Metamath Proof Explorer

Theorem salpreimalegt

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 
|- F/ x ph
salpreimalegt.a 
|- F/ a ph
salpreimalegt.s 
|- ( ph -> S e. SAlg )
salpreimalegt.u 
|- A = U. S
salpreimalegt.b 
|- ( ( ph /\ x e. A ) -> B e. RR* )
salpreimalegt.p 
|- ( ( ph /\ a e. RR ) -> { x e. A | B <_ a } e. S )
salpreimalegt.c 
|- ( ph -> C e. RR )
Assertion salpreimalegt 
|- ( ph -> { x e. A | C < B } e. S )

Proof

Step Hyp Ref Expression
1 salpreimalegt.x 
 |-  F/ x ph
2 salpreimalegt.a 
 |-  F/ a ph
3 salpreimalegt.s 
 |-  ( ph -> S e. SAlg )
4 salpreimalegt.u 
 |-  A = U. S
5 salpreimalegt.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
6 salpreimalegt.p 
 |-  ( ( ph /\ a e. RR ) -> { x e. A | B <_ a } e. S )
7 salpreimalegt.c 
 |-  ( ph -> C e. RR )
8 4 eqcomi 
 |-  U. S = A
9 8 a1i 
 |-  ( ph -> U. S = A )
10 9 difeq1d 
 |-  ( ph -> ( U. S \ { x e. A | B <_ C } ) = ( A \ { x e. A | B <_ C } ) )
11 7 rexrd 
 |-  ( ph -> C e. RR* )
12 1 5 11 preimalegt 
 |-  ( ph -> ( A \ { x e. A | B <_ C } ) = { x e. A | C < B } )
13 10 12 eqtr2d 
 |-  ( ph -> { x e. A | C < B } = ( U. S \ { x e. A | B <_ C } ) )
14 7 ancli 
 |-  ( ph -> ( ph /\ C e. RR ) )
15 nfv 
 |-  F/ a C e. RR
16 2 15 nfan 
 |-  F/ a ( ph /\ C e. RR )
17 nfv 
 |-  F/ a { x e. A | B <_ C } e. S
18 16 17 nfim 
 |-  F/ a ( ( ph /\ C e. RR ) -> { x e. A | B <_ C } e. S )
19 eleq1 
 |-  ( a = C -> ( a e. RR <-> C e. RR ) )
20 19 anbi2d 
 |-  ( a = C -> ( ( ph /\ a e. RR ) <-> ( ph /\ C e. RR ) ) )
21 breq2 
 |-  ( a = C -> ( B <_ a <-> B <_ C ) )
22 21 rabbidv 
 |-  ( a = C -> { x e. A | B <_ a } = { x e. A | B <_ C } )
23 22 eleq1d 
 |-  ( a = C -> ( { x e. A | B <_ a } e. S <-> { x e. A | B <_ C } e. S ) )
24 20 23 imbi12d 
 |-  ( a = C -> ( ( ( ph /\ a e. RR ) -> { x e. A | B <_ a } e. S ) <-> ( ( ph /\ C e. RR ) -> { x e. A | B <_ C } e. S ) ) )
25 18 24 6 vtoclg1f 
 |-  ( C e. RR -> ( ( ph /\ C e. RR ) -> { x e. A | B <_ C } e. S ) )
26 7 14 25 sylc 
 |-  ( ph -> { x e. A | B <_ C } e. S )
27 3 26 saldifcld 
 |-  ( ph -> ( U. S \ { x e. A | B <_ C } ) e. S )
28 13 27 eqeltrd 
 |-  ( ph -> { x e. A | C < B } e. S )