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

Proof

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