Theorem salpreimalegt

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

	Ref	Expression
Hypotheses	salpreimalegt.x	⊢ Ⅎ 𝑥 𝜑
	salpreimalegt.a	⊢ Ⅎ 𝑎 𝜑
	salpreimalegt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	salpreimalegt.u	⊢ 𝐴 = ∪ 𝑆
	salpreimalegt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
	salpreimalegt.p	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝑎 } ∈ 𝑆 )
	salpreimalegt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
Assertion	salpreimalegt	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ∈ 𝑆 )

Proof

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