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

Proof

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