Metamath Proof Explorer

Theorem salpreimagtge

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

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

Proof

Step Hyp Ref Expression
1 salpreimagtge.x 
 |-  F/ x ph
2 salpreimagtge.a 
 |-  F/ a ph
3 salpreimagtge.s 
 |-  ( ph -> S e. SAlg )
4 salpreimagtge.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
5 salpreimagtge.p 
 |-  ( ( ph /\ a e. RR ) -> { x e. A | a < B } e. S )
6 salpreimagtge.c 
 |-  ( ph -> C e. RR )
7 1 4 6 preimageiingt 
 |-  ( ph -> { x e. A | C <_ B } = |^|_ n e. NN { x e. A | ( C - ( 1 / n ) ) < B } )
8 nnct 
 |-  NN ~<_ _om
9 8 a1i 
 |-  ( ph -> NN ~<_ _om )
10 nnn0 
 |-  NN =/= (/)
11 10 a1i 
 |-  ( ph -> NN =/= (/) )
12 6 adantr 
 |-  ( ( ph /\ n e. NN ) -> C e. RR )
13 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
14 13 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / n ) e. RR )
15 12 14 resubcld 
 |-  ( ( ph /\ n e. NN ) -> ( C - ( 1 / n ) ) e. RR )
16 nfv 
 |-  F/ a ( C - ( 1 / n ) ) e. RR
17 2 16 nfan 
 |-  F/ a ( ph /\ ( C - ( 1 / n ) ) e. RR )
18 nfv 
 |-  F/ a { x e. A | ( C - ( 1 / n ) ) < B } e. S
19 17 18 nfim 
 |-  F/ a ( ( ph /\ ( C - ( 1 / n ) ) e. RR ) -> { x e. A | ( C - ( 1 / n ) ) < B } e. S )
20 ovex 
 |-  ( C - ( 1 / n ) ) e. _V
21 eleq1 
 |-  ( a = ( C - ( 1 / n ) ) -> ( a e. RR <-> ( C - ( 1 / n ) ) e. RR ) )
22 21 anbi2d 
 |-  ( a = ( C - ( 1 / n ) ) -> ( ( ph /\ a e. RR ) <-> ( ph /\ ( C - ( 1 / n ) ) e. RR ) ) )
23 breq1 
 |-  ( a = ( C - ( 1 / n ) ) -> ( a < B <-> ( C - ( 1 / n ) ) < B ) )
24 23 rabbidv 
 |-  ( a = ( C - ( 1 / n ) ) -> { x e. A | a < B } = { x e. A | ( C - ( 1 / n ) ) < B } )
25 24 eleq1d 
 |-  ( a = ( C - ( 1 / n ) ) -> ( { x e. A | a < B } e. S <-> { x e. A | ( C - ( 1 / n ) ) < B } e. S ) )
26 22 25 imbi12d 
 |-  ( a = ( C - ( 1 / n ) ) -> ( ( ( ph /\ a e. RR ) -> { x e. A | a < B } e. S ) <-> ( ( ph /\ ( C - ( 1 / n ) ) e. RR ) -> { x e. A | ( C - ( 1 / n ) ) < B } e. S ) ) )
27 19 20 26 5 vtoclf 
 |-  ( ( ph /\ ( C - ( 1 / n ) ) e. RR ) -> { x e. A | ( C - ( 1 / n ) ) < B } e. S )
28 15 27 syldan 
 |-  ( ( ph /\ n e. NN ) -> { x e. A | ( C - ( 1 / n ) ) < B } e. S )
29 3 9 11 28 saliincl 
 |-  ( ph -> |^|_ n e. NN { x e. A | ( C - ( 1 / n ) ) < B } e. S )
30 7 29 eqeltrd 
 |-  ( ph -> { x e. A | C <_ B } e. S )