Theorem salpreimagelt

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

	Ref	Expression
Hypotheses	salpreimagelt.x	$$⊢Ⅎx\phi$$
	salpreimagelt.a	$$⊢Ⅎa\phi$$
	salpreimagelt.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	salpreimagelt.u	$$⊢A=\bigcup S$$
	salpreimagelt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
	salpreimagelt.p	$$⊢\left(\phi \wedge a\in ℝ\right)\to \left\{x\in A|a\le B\right\}\in S$$
	salpreimagelt.c	$$⊢\phi \to C\in ℝ$$
Assertion	salpreimagelt	$$⊢\phi \to \left\{x\in A|B<C\right\}\in S$$

Proof

Step	Hyp	Ref	Expression
1		salpreimagelt.x	$$⊢Ⅎx\phi$$
2		salpreimagelt.a	$$⊢Ⅎa\phi$$
3		salpreimagelt.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
4		salpreimagelt.u	$$⊢A=\bigcup S$$
5		salpreimagelt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
6		salpreimagelt.p	$$⊢\left(\phi \wedge a\in ℝ\right)\to \left\{x\in A|a\le B\right\}\in S$$
7		salpreimagelt.c	$$⊢\phi \to C\in ℝ$$
8	4	eqcomi	$$⊢\bigcup S=A$$
9	8	a1i	$$⊢\phi \to \bigcup S=A$$
10	9	difeq1d	$$⊢\phi \to \bigcup S\setminus \left\{x\in A|C\le B\right\}=A\setminus \left\{x\in A|C\le B\right\}$$
11	7	rexrd	$$⊢\phi \to C\in {ℝ}^{*}$$
12	1 5 11	preimagelt	$$⊢\phi \to A\setminus \left\{x\in A|C\le B\right\}=\left\{x\in A|B<C\right\}$$
13	10 12	eqtr2d	$$⊢\phi \to \left\{x\in A|B<C\right\}=\bigcup S\setminus \left\{x\in A|C\le B\right\}$$
14	7	ancli	$$⊢\phi \to \left(\phi \wedge C\in ℝ\right)$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}aC$$
16	15	nfel1	$$⊢ℲaC\in ℝ$$
17	2 16	nfan	$$⊢Ⅎa\left(\phi \wedge C\in ℝ\right)$$
18		nfv	$$⊢Ⅎa\left\{x\in A|C\le B\right\}\in S$$
19	17 18	nfim	$$⊢Ⅎa\left(\left(\phi \wedge C\in ℝ\right)\to \left\{x\in A|C\le B\right\}\in S\right)$$
20		eleq1	$$⊢a=C\to \left(a\in ℝ\leftrightarrow C\in ℝ\right)$$
21	20	anbi2d	$$⊢a=C\to \left(\left(\phi \wedge a\in ℝ\right)\leftrightarrow \left(\phi \wedge C\in ℝ\right)\right)$$
22		breq1	$$⊢a=C\to \left(a\le B\leftrightarrow C\le B\right)$$
23	22	rabbidv	$$⊢a=C\to \left\{x\in A|a\le B\right\}=\left\{x\in A|C\le B\right\}$$
24	23	eleq1d	$$⊢a=C\to \left(\left\{x\in A|a\le B\right\}\in S\leftrightarrow \left\{x\in A|C\le B\right\}\in S\right)$$
25	21 24	imbi12d	$$⊢a=C\to \left(\left(\left(\phi \wedge a\in ℝ\right)\to \left\{x\in A|a\le B\right\}\in S\right)\leftrightarrow \left(\left(\phi \wedge C\in ℝ\right)\to \left\{x\in A|C\le B\right\}\in S\right)\right)$$
26	19 25 6	vtoclg1f	$$⊢C\in ℝ\to \left(\left(\phi \wedge C\in ℝ\right)\to \left\{x\in A|C\le B\right\}\in S\right)$$
27	7 14 26	sylc	$$⊢\phi \to \left\{x\in A|C\le B\right\}\in S$$
28	3 27	saldifcld	$$⊢\phi \to \bigcup S\setminus \left\{x\in A|C\le B\right\}\in S$$
29	13 28	eqeltrd	$$⊢\phi \to \left\{x\in A|B<C\right\}\in S$$