Theorem salpreimalelt

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

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

Proof

Step	Hyp	Ref	Expression
1		salpreimalelt.x	|- F/ x ph
2		salpreimalelt.a	|- F/ a ph
3		salpreimalelt.s	|- ( ph -> S e. SAlg )
4		salpreimalelt.u	|- A = U. S
5		salpreimalelt.b	|- ( ( ph /\ x e. A ) -> B e. RR* )
6		salpreimalelt.p	|- ( ( ph /\ a e. RR ) -> { x e. A | B <_ a } e. S )
7		salpreimalelt.c	|- ( ph -> C e. RR )
8		nfv	|- F/ x a e. RR
9	1 8	nfan	|- F/ x ( ph /\ a e. RR )
10		nfv	|- F/ b ( ph /\ a e. RR )
11	3	adantr	|- ( ( ph /\ a e. RR ) -> S e. SAlg )
12	5	adantlr	|- ( ( ( ph /\ a e. RR ) /\ x e. A ) -> B e. RR* )
13		nfv	|- F/ x b e. RR
14	1 13	nfan	|- F/ x ( ph /\ b e. RR )
15		nfv	|- F/ a b e. RR
16	2 15	nfan	|- F/ a ( ph /\ b e. RR )
17	3	adantr	|- ( ( ph /\ b e. RR ) -> S e. SAlg )
18	5	adantlr	|- ( ( ( ph /\ b e. RR ) /\ x e. A ) -> B e. RR* )
19	6	adantlr	|- ( ( ( ph /\ b e. RR ) /\ a e. RR ) -> { x e. A | B <_ a } e. S )
20		simpr	|- ( ( ph /\ b e. RR ) -> b e. RR )
21	14 16 17 4 18 19 20	salpreimalegt	|- ( ( ph /\ b e. RR ) -> { x e. A | b < B } e. S )
22	21	adantlr	|- ( ( ( ph /\ a e. RR ) /\ b e. RR ) -> { x e. A | b < B } e. S )
23		simpr	|- ( ( ph /\ a e. RR ) -> a e. RR )
24	9 10 11 12 22 23	salpreimagtge	|- ( ( ph /\ a e. RR ) -> { x e. A | a <_ B } e. S )
25	1 2 3 4 5 24 7	salpreimagelt	|- ( ph -> { x e. A | B < C } e. S )