Metamath Proof Explorer


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φ
preimagelt.b φxAB*
preimagelt.c φC*
Assertion preimagelt φAxA|CB=xA|B<C

Proof

Step Hyp Ref Expression
1 preimagelt.x xφ
2 preimagelt.b φxAB*
3 preimagelt.c φC*
4 nfcv _xA
5 nfrab1 _xxA|CB
6 4 5 nfdif _xAxA|CB
7 nfrab1 _xxA|B<C
8 eldifi xAxA|CBxA
9 8 adantl φxAxA|CBxA
10 eldifn xAxA|CB¬xxA|CB
11 8 anim1i xAxA|CBCBxACB
12 rabid xxA|CBxACB
13 11 12 sylibr xAxA|CBCBxxA|CB
14 10 13 mtand xAxA|CB¬CB
15 14 adantl φxAxA|CB¬CB
16 8 2 sylan2 φxAxA|CBB*
17 3 adantr φxAxA|CBC*
18 16 17 xrltnled φxAxA|CBB<C¬CB
19 15 18 mpbird φxAxA|CBB<C
20 rabid xxA|B<CxAB<C
21 9 19 20 sylanbrc φxAxA|CBxxA|B<C
22 rabidim1 xxA|B<CxA
23 22 adantl φxxA|B<CxA
24 rabidim2 xxA|B<CB<C
25 24 adantl φxxA|B<CB<C
26 22 2 sylan2 φxxA|B<CB*
27 3 adantr φxxA|B<CC*
28 26 27 xrltnled φxxA|B<CB<C¬CB
29 25 28 mpbid φxxA|B<C¬CB
30 29 intnand φxxA|B<C¬xACB
31 30 12 sylnibr φxxA|B<C¬xxA|CB
32 23 31 eldifd φxxA|B<CxAxA|CB
33 21 32 impbida φxAxA|CBxxA|B<C
34 1 6 7 33 eqrd φAxA|CB=xA|B<C