Metamath Proof Explorer

Theorem salpreimaltle

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

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

Proof

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