Theorem salpreimalegt

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

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

Proof

Step	Hyp	Ref	Expression
1		salpreimalegt.x	$$⊢Ⅎx\phi$$
2		salpreimalegt.a	$$⊢Ⅎa\phi$$
3		salpreimalegt.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
4		salpreimalegt.u	$$⊢A=\bigcup S$$
5		salpreimalegt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
6		salpreimalegt.p	$$⊢\left(\phi \wedge a\in ℝ\right)\to \left\{x\in A|B\le a\right\}\in S$$
7		salpreimalegt.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|B\le C\right\}=A\setminus \left\{x\in A|B\le C\right\}$$
11	7	rexrd	$$⊢\phi \to C\in {ℝ}^{*}$$
12	1 5 11	preimalegt	$$⊢\phi \to A\setminus \left\{x\in A|B\le C\right\}=\left\{x\in A|C<B\right\}$$
13	10 12	eqtr2d	$$⊢\phi \to \left\{x\in A|C<B\right\}=\bigcup S\setminus \left\{x\in A|B\le C\right\}$$
14	7	ancli	$$⊢\phi \to \left(\phi \wedge C\in ℝ\right)$$
15		nfv	$$⊢ℲaC\in ℝ$$
16	2 15	nfan	$$⊢Ⅎa\left(\phi \wedge C\in ℝ\right)$$
17		nfv	$$⊢Ⅎa\left\{x\in A|B\le C\right\}\in S$$
18	16 17	nfim	$$⊢Ⅎa\left(\left(\phi \wedge C\in ℝ\right)\to \left\{x\in A|B\le C\right\}\in S\right)$$
19		eleq1	$$⊢a=C\to \left(a\in ℝ\leftrightarrow C\in ℝ\right)$$
20	19	anbi2d	$$⊢a=C\to \left(\left(\phi \wedge a\in ℝ\right)\leftrightarrow \left(\phi \wedge C\in ℝ\right)\right)$$
21		breq2	$$⊢a=C\to \left(B\le a\leftrightarrow B\le C\right)$$
22	21	rabbidv	$$⊢a=C\to \left\{x\in A|B\le a\right\}=\left\{x\in A|B\le C\right\}$$
23	22	eleq1d	$$⊢a=C\to \left(\left\{x\in A|B\le a\right\}\in S\leftrightarrow \left\{x\in A|B\le C\right\}\in S\right)$$
24	20 23	imbi12d	$$⊢a=C\to \left(\left(\left(\phi \wedge a\in ℝ\right)\to \left\{x\in A|B\le a\right\}\in S\right)\leftrightarrow \left(\left(\phi \wedge C\in ℝ\right)\to \left\{x\in A|B\le C\right\}\in S\right)\right)$$
25	18 24 6	vtoclg1f	$$⊢C\in ℝ\to \left(\left(\phi \wedge C\in ℝ\right)\to \left\{x\in A|B\le C\right\}\in S\right)$$
26	7 14 25	sylc	$$⊢\phi \to \left\{x\in A|B\le C\right\}\in S$$
27	3 26	saldifcld	$$⊢\phi \to \bigcup S\setminus \left\{x\in A|B\le C\right\}\in S$$
28	13 27	eqeltrd	$$⊢\phi \to \left\{x\in A|C<B\right\}\in S$$