Theorem salpreimagtge

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

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

Proof

Step	Hyp	Ref	Expression
1		salpreimagtge.x	⊢ Ⅎ 𝑥 𝜑
2		salpreimagtge.a	⊢ Ⅎ 𝑎 𝜑
3		salpreimagtge.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		salpreimagtge.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
5		salpreimagtge.p	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝑎 < 𝐵 } ∈ 𝑆 )
6		salpreimagtge.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
7	1 4 6	preimageiingt	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } = ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } )
8		nnct	⊢ ℕ ≼ ω
9	8	a1i	⊢ ( 𝜑 → ℕ ≼ ω )
10		nnn0	⊢ ℕ ≠ ∅
11	10	a1i	⊢ ( 𝜑 → ℕ ≠ ∅ )
12	6	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ℝ )
13		nnrecre	⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ )
15	12 14	resubcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 − ( 1 / 𝑛 ) ) ∈ ℝ )
16		nfv	⊢ Ⅎ 𝑎 ( 𝐶 − ( 1 / 𝑛 ) ) ∈ ℝ
17	2 16	nfan	⊢ Ⅎ 𝑎 ( 𝜑 ∧ ( 𝐶 − ( 1 / 𝑛 ) ) ∈ ℝ )
18		nfv	⊢ Ⅎ 𝑎 { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } ∈ 𝑆
19	17 18	nfim	⊢ Ⅎ 𝑎 ( ( 𝜑 ∧ ( 𝐶 − ( 1 / 𝑛 ) ) ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } ∈ 𝑆 )
20		ovex	⊢ ( 𝐶 − ( 1 / 𝑛 ) ) ∈ V
21		eleq1	⊢ ( 𝑎 = ( 𝐶 − ( 1 / 𝑛 ) ) → ( 𝑎 ∈ ℝ ↔ ( 𝐶 − ( 1 / 𝑛 ) ) ∈ ℝ ) )
22	21	anbi2d	⊢ ( 𝑎 = ( 𝐶 − ( 1 / 𝑛 ) ) → ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ↔ ( 𝜑 ∧ ( 𝐶 − ( 1 / 𝑛 ) ) ∈ ℝ ) ) )
23		breq1	⊢ ( 𝑎 = ( 𝐶 − ( 1 / 𝑛 ) ) → ( 𝑎 < 𝐵 ↔ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) )
24	23	rabbidv	⊢ ( 𝑎 = ( 𝐶 − ( 1 / 𝑛 ) ) → { 𝑥 ∈ 𝐴 ∣ 𝑎 < 𝐵 } = { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } )
25	24	eleq1d	⊢ ( 𝑎 = ( 𝐶 − ( 1 / 𝑛 ) ) → ( { 𝑥 ∈ 𝐴 ∣ 𝑎 < 𝐵 } ∈ 𝑆 ↔ { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } ∈ 𝑆 ) )
26	22 25	imbi12d	⊢ ( 𝑎 = ( 𝐶 − ( 1 / 𝑛 ) ) → ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝑎 < 𝐵 } ∈ 𝑆 ) ↔ ( ( 𝜑 ∧ ( 𝐶 − ( 1 / 𝑛 ) ) ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } ∈ 𝑆 ) ) )
27	19 20 26 5	vtoclf	⊢ ( ( 𝜑 ∧ ( 𝐶 − ( 1 / 𝑛 ) ) ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } ∈ 𝑆 )
28	15 27	syldan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } ∈ 𝑆 )
29	3 9 11 28	saliincl	⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } ∈ 𝑆 )
30	7 29	eqeltrd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ∈ 𝑆 )