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 | |
|
preimagelt.b | |
||
preimagelt.c | |
||
Assertion | preimagelt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | preimagelt.x | |
|
2 | preimagelt.b | |
|
3 | preimagelt.c | |
|
4 | nfcv | |
|
5 | nfrab1 | |
|
6 | 4 5 | nfdif | |
7 | nfrab1 | |
|
8 | eldifi | |
|
9 | 8 | adantl | |
10 | eldifn | |
|
11 | 8 | anim1i | |
12 | rabid | |
|
13 | 11 12 | sylibr | |
14 | 10 13 | mtand | |
15 | 14 | adantl | |
16 | 8 2 | sylan2 | |
17 | 3 | adantr | |
18 | 16 17 | xrltnled | |
19 | 15 18 | mpbird | |
20 | rabid | |
|
21 | 9 19 20 | sylanbrc | |
22 | rabidim1 | |
|
23 | 22 | adantl | |
24 | rabidim2 | |
|
25 | 24 | adantl | |
26 | 22 2 | sylan2 | |
27 | 3 | adantr | |
28 | 26 27 | xrltnled | |
29 | 25 28 | mpbid | |
30 | 29 | intnand | |
31 | 30 12 | sylnibr | |
32 | 23 31 | eldifd | |
33 | 21 32 | impbida | |
34 | 1 6 7 33 | eqrd | |