Theorem salpreimagtlt

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

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

Proof

Step	Hyp	Ref	Expression
1		salpreimagtlt.x	|- F/ x ph
2		salpreimagtlt.a	|- F/ a ph
3		salpreimagtlt.s	|- ( ph -> S e. SAlg )
4		salpreimagtlt.u	|- A = U. S
5		salpreimagtlt.b	|- ( ( ph /\ x e. A ) -> B e. RR* )
6		salpreimagtlt.p	|- ( ( ph /\ a e. RR ) -> { x e. A | a < B } e. S )
7		salpreimagtlt.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/ a b e. RR
14	2 13	nfan	|- F/ a ( ph /\ b e. RR )
15		nfv	|- F/ a { x e. A | b < B } e. S
16	14 15	nfim	|- F/ a ( ( ph /\ b e. RR ) -> { x e. A | b < B } e. S )
17		eleq1w	|- ( a = b -> ( a e. RR <-> b e. RR ) )
18	17	anbi2d	|- ( a = b -> ( ( ph /\ a e. RR ) <-> ( ph /\ b e. RR ) ) )
19		breq1	|- ( a = b -> ( a < B <-> b < B ) )
20	19	rabbidv	|- ( a = b -> { x e. A | a < B } = { x e. A | b < B } )
21	20	eleq1d	|- ( a = b -> ( { x e. A | a < B } e. S <-> { x e. A | b < B } e. S ) )
22	18 21	imbi12d	|- ( a = b -> ( ( ( ph /\ a e. RR ) -> { x e. A | a < B } e. S ) <-> ( ( ph /\ b e. RR ) -> { x e. A | b < B } e. S ) ) )
23	16 22 6	chvarfv	|- ( ( ph /\ b e. RR ) -> { x e. A | b < B } e. S )
24	23	adantlr	|- ( ( ( ph /\ a e. RR ) /\ b e. RR ) -> { x e. A | b < B } e. S )
25		simpr	|- ( ( ph /\ a e. RR ) -> a e. RR )
26	9 10 11 12 24 25	salpreimagtge	|- ( ( ph /\ a e. RR ) -> { x e. A | a <_ B } e. S )
27	1 2 3 4 5 26 7	salpreimagelt	|- ( ph -> { x e. A | B < C } e. S )