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

Proof

Step	Hyp	Ref	Expression
1		salpreimalelt.x	⊢ Ⅎ 𝑥 𝜑
2		salpreimalelt.a	⊢ Ⅎ 𝑎 𝜑
3		salpreimalelt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		salpreimalelt.u	⊢ 𝐴 = ∪ 𝑆
5		salpreimalelt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
6		salpreimalelt.p	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝑎 } ∈ 𝑆 )
7		salpreimalelt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
8		nfv	⊢ Ⅎ 𝑥 𝑎 ∈ ℝ
9	1 8	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑎 ∈ ℝ )
10		nfv	⊢ Ⅎ 𝑏 ( 𝜑 ∧ 𝑎 ∈ ℝ )
11	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑆 ∈ SAlg )
12	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
13		nfv	⊢ Ⅎ 𝑥 𝑏 ∈ ℝ
14	1 13	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑏 ∈ ℝ )
15		nfv	⊢ Ⅎ 𝑎 𝑏 ∈ ℝ
16	2 15	nfan	⊢ Ⅎ 𝑎 ( 𝜑 ∧ 𝑏 ∈ ℝ )
17	3	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → 𝑆 ∈ SAlg )
18	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
19	6	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝑎 } ∈ 𝑆 )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → 𝑏 ∈ ℝ )
21	14 16 17 4 18 19 20	salpreimalegt	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝑏 < 𝐵 } ∈ 𝑆 )
22	21	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑏 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝑏 < 𝐵 } ∈ 𝑆 )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
24	9 10 11 12 22 23	salpreimagtge	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝑎 ≤ 𝐵 } ∈ 𝑆 )
25	1 2 3 4 5 24 7	salpreimagelt	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∈ 𝑆 )