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	$$⊢Ⅎx\phi$$
	salpreimalelt.a	$$⊢Ⅎa\phi$$
	salpreimalelt.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	salpreimalelt.u	$$⊢A=\bigcup S$$
	salpreimalelt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
	salpreimalelt.p	$$⊢\left(\phi \wedge a\in ℝ\right)\to \left\{x\in A|B\le a\right\}\in S$$
	salpreimalelt.c	$$⊢\phi \to C\in ℝ$$
Assertion	salpreimalelt	$$⊢\phi \to \left\{x\in A|B<C\right\}\in S$$

Proof

Step	Hyp	Ref	Expression
1		salpreimalelt.x	$$⊢Ⅎx\phi$$
2		salpreimalelt.a	$$⊢Ⅎa\phi$$
3		salpreimalelt.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
4		salpreimalelt.u	$$⊢A=\bigcup S$$
5		salpreimalelt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
6		salpreimalelt.p	$$⊢\left(\phi \wedge a\in ℝ\right)\to \left\{x\in A|B\le a\right\}\in S$$
7		salpreimalelt.c	$$⊢\phi \to C\in ℝ$$
8		nfv	$$⊢Ⅎxa\in ℝ$$
9	1 8	nfan	$$⊢Ⅎx\left(\phi \wedge a\in ℝ\right)$$
10		nfv	$$⊢Ⅎb\left(\phi \wedge a\in ℝ\right)$$
11	3	adantr	$$⊢\left(\phi \wedge a\in ℝ\right)\to S\in \mathrm{SAlg}$$
12	5	adantlr	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge x\in A\right)\to B\in {ℝ}^{*}$$
13		nfv	$$⊢Ⅎxb\in ℝ$$
14	1 13	nfan	$$⊢Ⅎx\left(\phi \wedge b\in ℝ\right)$$
15		nfv	$$⊢Ⅎab\in ℝ$$
16	2 15	nfan	$$⊢Ⅎa\left(\phi \wedge b\in ℝ\right)$$
17	3	adantr	$$⊢\left(\phi \wedge b\in ℝ\right)\to S\in \mathrm{SAlg}$$
18	5	adantlr	$$⊢\left(\left(\phi \wedge b\in ℝ\right)\wedge x\in A\right)\to B\in {ℝ}^{*}$$
19	6	adantlr	$$⊢\left(\left(\phi \wedge b\in ℝ\right)\wedge a\in ℝ\right)\to \left\{x\in A|B\le a\right\}\in S$$
20		simpr	$$⊢\left(\phi \wedge b\in ℝ\right)\to b\in ℝ$$
21	14 16 17 4 18 19 20	salpreimalegt	$$⊢\left(\phi \wedge b\in ℝ\right)\to \left\{x\in A|b<B\right\}\in S$$
22	21	adantlr	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge b\in ℝ\right)\to \left\{x\in A|b<B\right\}\in S$$
23		simpr	$$⊢\left(\phi \wedge a\in ℝ\right)\to a\in ℝ$$
24	9 10 11 12 22 23	salpreimagtge	$$⊢\left(\phi \wedge a\in ℝ\right)\to \left\{x\in A|a\le B\right\}\in S$$
25	1 2 3 4 5 24 7	salpreimagelt	$$⊢\phi \to \left\{x\in A|B<C\right\}\in S$$