Metamath Proof Explorer

Theorem salpreimagelt

Description: If all the preimages of left-closed, unbounded below intervals, belong to a sigma-algebra, then all the preimages of right-open, unbounded below intervals, belong to the sigma-algebra. (iv) implies (i) in Proposition 121B of Fremlin1 p. 36. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses salpreimagelt.x 
|- F/ x ph
salpreimagelt.a 
|- F/ a ph
salpreimagelt.s 
|- ( ph -> S e. SAlg )
salpreimagelt.u 
|- A = U. S
salpreimagelt.b 
|- ( ( ph /\ x e. A ) -> B e. RR* )
salpreimagelt.p 
|- ( ( ph /\ a e. RR ) -> { x e. A | a <_ B } e. S )
salpreimagelt.c 
|- ( ph -> C e. RR )
Assertion salpreimagelt 
|- ( ph -> { x e. A | B < C } e. S )

Proof

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