Theorem preimalegt

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

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

Proof

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