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	⊢ Ⅎ 𝑥 𝜑
	salpreimagelt.a	⊢ Ⅎ 𝑎 𝜑
	salpreimagelt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	salpreimagelt.u	⊢ 𝐴 = ∪ 𝑆
	salpreimagelt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
	salpreimagelt.p	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝑎 ≤ 𝐵 } ∈ 𝑆 )
	salpreimagelt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
Assertion	salpreimagelt	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		salpreimagelt.x	⊢ Ⅎ 𝑥 𝜑
2		salpreimagelt.a	⊢ Ⅎ 𝑎 𝜑
3		salpreimagelt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		salpreimagelt.u	⊢ 𝐴 = ∪ 𝑆
5		salpreimagelt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
6		salpreimagelt.p	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝑎 ≤ 𝐵 } ∈ 𝑆 )
7		salpreimagelt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
8	4	eqcomi	⊢ ∪ 𝑆 = 𝐴
9	8	a1i	⊢ ( 𝜑 → ∪ 𝑆 = 𝐴 )
10	9	difeq1d	⊢ ( 𝜑 → ( ∪ 𝑆 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) = ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) )
11	7	rexrd	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
12	1 5 11	preimagelt	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } )
13	10 12	eqtr2d	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } = ( ∪ 𝑆 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) )
14	7	ancli	⊢ ( 𝜑 → ( 𝜑 ∧ 𝐶 ∈ ℝ ) )
15		nfcv	⊢ Ⅎ 𝑎 𝐶
16	15	nfel1	⊢ Ⅎ 𝑎 𝐶 ∈ ℝ
17	2 16	nfan	⊢ Ⅎ 𝑎 ( 𝜑 ∧ 𝐶 ∈ ℝ )
18		nfv	⊢ Ⅎ 𝑎 { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ∈ 𝑆
19	17 18	nfim	⊢ Ⅎ 𝑎 ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ∈ 𝑆 )
20		eleq1	⊢ ( 𝑎 = 𝐶 → ( 𝑎 ∈ ℝ ↔ 𝐶 ∈ ℝ ) )
21	20	anbi2d	⊢ ( 𝑎 = 𝐶 → ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ↔ ( 𝜑 ∧ 𝐶 ∈ ℝ ) ) )
22		breq1	⊢ ( 𝑎 = 𝐶 → ( 𝑎 ≤ 𝐵 ↔ 𝐶 ≤ 𝐵 ) )
23	22	rabbidv	⊢ ( 𝑎 = 𝐶 → { 𝑥 ∈ 𝐴 ∣ 𝑎 ≤ 𝐵 } = { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } )
24	23	eleq1d	⊢ ( 𝑎 = 𝐶 → ( { 𝑥 ∈ 𝐴 ∣ 𝑎 ≤ 𝐵 } ∈ 𝑆 ↔ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ∈ 𝑆 ) )
25	21 24	imbi12d	⊢ ( 𝑎 = 𝐶 → ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝑎 ≤ 𝐵 } ∈ 𝑆 ) ↔ ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ∈ 𝑆 ) ) )
26	19 25 6	vtoclg1f	⊢ ( 𝐶 ∈ ℝ → ( ( 𝜑 ∧ 𝐶 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ∈ 𝑆 ) )
27	7 14 26	sylc	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ∈ 𝑆 )
28	3 27	saldifcld	⊢ ( 𝜑 → ( ∪ 𝑆 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) ∈ 𝑆 )
29	13 28	eqeltrd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∈ 𝑆 )