Metamath Proof Explorer


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 φ
preimalegt.b φ x A B *
preimalegt.c φ C *
Assertion preimalegt φ A x A | B C = x A | C < B

Proof

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