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

Proof

Step	Hyp	Ref	Expression
1		salpreimagtlt.x	$$⊢Ⅎx\phi$$
2		salpreimagtlt.a	$$⊢Ⅎa\phi$$
3		salpreimagtlt.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
4		salpreimagtlt.u	$$⊢A=\bigcup S$$
5		salpreimagtlt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
6		salpreimagtlt.p	$$⊢\left(\phi \wedge a\in ℝ\right)\to \left\{x\in A|a<B\right\}\in S$$
7		salpreimagtlt.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	$$⊢Ⅎab\in ℝ$$
14	2 13	nfan	$$⊢Ⅎa\left(\phi \wedge b\in ℝ\right)$$
15		nfv	$$⊢Ⅎa\left\{x\in A|b<B\right\}\in S$$
16	14 15	nfim	$$⊢Ⅎa\left(\left(\phi \wedge b\in ℝ\right)\to \left\{x\in A|b<B\right\}\in S\right)$$
17		eleq1w	$$⊢a=b\to \left(a\in ℝ\leftrightarrow b\in ℝ\right)$$
18	17	anbi2d	$$⊢a=b\to \left(\left(\phi \wedge a\in ℝ\right)\leftrightarrow \left(\phi \wedge b\in ℝ\right)\right)$$
19		breq1	$$⊢a=b\to \left(a<B\leftrightarrow b<B\right)$$
20	19	rabbidv	$$⊢a=b\to \left\{x\in A|a<B\right\}=\left\{x\in A|b<B\right\}$$
21	20	eleq1d	$$⊢a=b\to \left(\left\{x\in A|a<B\right\}\in S\leftrightarrow \left\{x\in A|b<B\right\}\in S\right)$$
22	18 21	imbi12d	$$⊢a=b\to \left(\left(\left(\phi \wedge a\in ℝ\right)\to \left\{x\in A|a<B\right\}\in S\right)\leftrightarrow \left(\left(\phi \wedge b\in ℝ\right)\to \left\{x\in A|b<B\right\}\in S\right)\right)$$
23	16 22 6	chvarfv	$$⊢\left(\phi \wedge b\in ℝ\right)\to \left\{x\in A|b<B\right\}\in S$$
24	23	adantlr	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge b\in ℝ\right)\to \left\{x\in A|b<B\right\}\in S$$
25		simpr	$$⊢\left(\phi \wedge a\in ℝ\right)\to a\in ℝ$$
26	9 10 11 12 24 25	salpreimagtge	$$⊢\left(\phi \wedge a\in ℝ\right)\to \left\{x\in A|a\le B\right\}\in S$$
27	1 2 3 4 5 26 7	salpreimagelt	$$⊢\phi \to \left\{x\in A|B<C\right\}\in S$$