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	|- F/ x ph
	preimalegt.b	|- ( ( ph /\ x e. A ) -> B e. RR* )
	preimalegt.c	|- ( ph -> C e. RR* )
Assertion	preimalegt	|- ( ph -> ( A \ { x e. A | B <_ C } ) = { x e. A | C < B } )

Proof

Step	Hyp	Ref	Expression
1		preimalegt.x	|- F/ x ph
2		preimalegt.b	|- ( ( ph /\ x e. A ) -> B e. RR* )
3		preimalegt.c	|- ( ph -> C e. RR* )
4		nfcv	|- F/_ x A
5		nfrab1	|- F/_ x { x e. A | B <_ C }
6	4 5	nfdif	|- F/_ x ( A \ { x e. A | B <_ C } )
7		nfrab1	|- F/_ x { x e. A | C < B }
8		eldifi	|- ( x e. ( A \ { x e. A | B <_ C } ) -> x e. A )
9	8	adantl	|- ( ( ph /\ x e. ( A \ { x e. A | B <_ C } ) ) -> x e. A )
10		eldifn	|- ( x e. ( A \ { x e. A | B <_ C } ) -> -. x e. { x e. A | B <_ C } )
11	8	anim1i	|- ( ( x e. ( A \ { x e. A | B <_ C } ) /\ B <_ C ) -> ( x e. A /\ B <_ C ) )
12		rabid	|- ( x e. { x e. A | B <_ C } <-> ( x e. A /\ B <_ C ) )
13	11 12	sylibr	|- ( ( x e. ( A \ { x e. A | B <_ C } ) /\ B <_ C ) -> x e. { x e. A | B <_ C } )
14	10 13	mtand	|- ( x e. ( A \ { x e. A | B <_ C } ) -> -. B <_ C )
15	14	adantl	|- ( ( ph /\ x e. ( A \ { x e. A | B <_ C } ) ) -> -. B <_ C )
16	3	adantr	|- ( ( ph /\ x e. ( A \ { x e. A | B <_ C } ) ) -> C e. RR* )
17	8 2	sylan2	|- ( ( ph /\ x e. ( A \ { x e. A | B <_ C } ) ) -> B e. RR* )
18	16 17	xrltnled	|- ( ( ph /\ x e. ( A \ { x e. A | B <_ C } ) ) -> ( C < B <-> -. B <_ C ) )
19	15 18	mpbird	|- ( ( ph /\ x e. ( A \ { x e. A | B <_ C } ) ) -> C < B )
20		rabid	|- ( x e. { x e. A | C < B } <-> ( x e. A /\ C < B ) )
21	9 19 20	sylanbrc	|- ( ( ph /\ x e. ( A \ { x e. A | B <_ C } ) ) -> x e. { x e. A | C < B } )
22		rabidim1	|- ( x e. { x e. A | C < B } -> x e. A )
23	22	adantl	|- ( ( ph /\ x e. { x e. A | C < B } ) -> x e. A )
24		rabidim2	|- ( x e. { x e. A | C < B } -> C < B )
25	24	adantl	|- ( ( ph /\ x e. { x e. A | C < B } ) -> C < B )
26	3	adantr	|- ( ( ph /\ x e. { x e. A | C < B } ) -> C e. RR* )
27	22 2	sylan2	|- ( ( ph /\ x e. { x e. A | C < B } ) -> B e. RR* )
28	26 27	xrltnled	|- ( ( ph /\ x e. { x e. A | C < B } ) -> ( C < B <-> -. B <_ C ) )
29	25 28	mpbid	|- ( ( ph /\ x e. { x e. A | C < B } ) -> -. B <_ C )
30	29	intnand	|- ( ( ph /\ x e. { x e. A | C < B } ) -> -. ( x e. A /\ B <_ C ) )
31	30 12	sylnibr	|- ( ( ph /\ x e. { x e. A | C < B } ) -> -. x e. { x e. A | B <_ C } )
32	23 31	eldifd	|- ( ( ph /\ x e. { x e. A | C < B } ) -> x e. ( A \ { x e. A | B <_ C } ) )
33	21 32	impbida	|- ( ph -> ( x e. ( A \ { x e. A | B <_ C } ) <-> x e. { x e. A | C < B } ) )
34	1 6 7 33	eqrd	|- ( ph -> ( A \ { x e. A | B <_ C } ) = { x e. A | C < B } )