Theorem preimagelt

Description: The preimage of a right-open, unbounded below interval, is the complement of a left-closed unbounded above interval. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	preimagelt.x	$$⊢Ⅎx\phi$$
	preimagelt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
	preimagelt.c	$$⊢\phi \to C\in {ℝ}^{*}$$
Assertion	preimagelt	$$⊢\phi \to A\setminus \left\{x\in A|C\le B\right\}=\left\{x\in A|B<C\right\}$$

Proof

Step	Hyp	Ref	Expression
1		preimagelt.x	$$⊢Ⅎx\phi$$
2		preimagelt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
3		preimagelt.c	$$⊢\phi \to C\in {ℝ}^{*}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
5		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|C\le B\right\}$$
6	4 5	nfdif	$$⊢\underset{\_}{Ⅎ}x\left(A\setminus \left\{x\in A|C\le B\right\}\right)$$
7		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|B<C\right\}$$
8		eldifi	$$⊢x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)\to x\in A$$
9	8	adantl	$$⊢\left(\phi \wedge x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)\right)\to x\in A$$
10		eldifn	$$⊢x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)\to \neg x\in \left\{x\in A|C\le B\right\}$$
11	8	anim1i	$$⊢\left(x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)\wedge C\le B\right)\to \left(x\in A\wedge C\le B\right)$$
12		rabid	$$⊢x\in \left\{x\in A|C\le B\right\}\leftrightarrow \left(x\in A\wedge C\le B\right)$$
13	11 12	sylibr	$$⊢\left(x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)\wedge C\le B\right)\to x\in \left\{x\in A|C\le B\right\}$$
14	10 13	mtand	$$⊢x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)\to \neg C\le B$$
15	14	adantl	$$⊢\left(\phi \wedge x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)\right)\to \neg C\le B$$
16	8 2	sylan2	$$⊢\left(\phi \wedge x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)\right)\to B\in {ℝ}^{*}$$
17	3	adantr	$$⊢\left(\phi \wedge x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)\right)\to C\in {ℝ}^{*}$$
18	16 17	xrltnled	$$⊢\left(\phi \wedge x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)\right)\to \left(B<C\leftrightarrow \neg C\le B\right)$$
19	15 18	mpbird	$$⊢\left(\phi \wedge x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)\right)\to B<C$$
20		rabid	$$⊢x\in \left\{x\in A|B<C\right\}\leftrightarrow \left(x\in A\wedge B<C\right)$$
21	9 19 20	sylanbrc	$$⊢\left(\phi \wedge x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)\right)\to x\in \left\{x\in A|B<C\right\}$$
22		rabidim1	$$⊢x\in \left\{x\in A|B<C\right\}\to x\in A$$
23	22	adantl	$$⊢\left(\phi \wedge x\in \left\{x\in A|B<C\right\}\right)\to x\in A$$
24		rabidim2	$$⊢x\in \left\{x\in A|B<C\right\}\to B<C$$
25	24	adantl	$$⊢\left(\phi \wedge x\in \left\{x\in A|B<C\right\}\right)\to B<C$$
26	22 2	sylan2	$$⊢\left(\phi \wedge x\in \left\{x\in A|B<C\right\}\right)\to B\in {ℝ}^{*}$$
27	3	adantr	$$⊢\left(\phi \wedge x\in \left\{x\in A|B<C\right\}\right)\to C\in {ℝ}^{*}$$
28	26 27	xrltnled	$$⊢\left(\phi \wedge x\in \left\{x\in A|B<C\right\}\right)\to \left(B<C\leftrightarrow \neg C\le B\right)$$
29	25 28	mpbid	$$⊢\left(\phi \wedge x\in \left\{x\in A|B<C\right\}\right)\to \neg C\le B$$
30	29	intnand	$$⊢\left(\phi \wedge x\in \left\{x\in A|B<C\right\}\right)\to \neg \left(x\in A\wedge C\le B\right)$$
31	30 12	sylnibr	$$⊢\left(\phi \wedge x\in \left\{x\in A|B<C\right\}\right)\to \neg x\in \left\{x\in A|C\le B\right\}$$
32	23 31	eldifd	$$⊢\left(\phi \wedge x\in \left\{x\in A|B<C\right\}\right)\to x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)$$
33	21 32	impbida	$$⊢\phi \to \left(x\in \left(A\setminus \left\{x\in A|C\le B\right\}\right)\leftrightarrow x\in \left\{x\in A|B<C\right\}\right)$$
34	1 6 7 33	eqrd	$$⊢\phi \to A\setminus \left\{x\in A|C\le B\right\}=\left\{x\in A|B<C\right\}$$