Metamath Proof Explorer


Theorem elicores

Description: Membership in a left-closed, right-open interval with real bounds. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion elicores A ran . 2 x y A = x y

Proof

Step Hyp Ref Expression
1 df-ico . = x * , y * z * | x z z < y
2 1 reseq1i . 2 = x * , y * z * | x z z < y 2
3 ressxr *
4 resmpo * * x * , y * z * | x z z < y 2 = x , y z * | x z z < y
5 3 3 4 mp2an x * , y * z * | x z z < y 2 = x , y z * | x z z < y
6 2 5 eqtri . 2 = x , y z * | x z z < y
7 6 rneqi ran . 2 = ran x , y z * | x z z < y
8 7 eleq2i A ran . 2 A ran x , y z * | x z z < y
9 eqid x , y z * | x z z < y = x , y z * | x z z < y
10 xrex * V
11 10 rabex z * | x z z < y V
12 9 11 elrnmpo A ran x , y z * | x z z < y x y A = z * | x z z < y
13 3 sseli x x *
14 13 adantr x y x *
15 3 sseli y y *
16 15 adantl x y y *
17 icoval x * y * x y = z * | x z z < y
18 14 16 17 syl2anc x y x y = z * | x z z < y
19 18 eqcomd x y z * | x z z < y = x y
20 19 eqeq2d x y A = z * | x z z < y A = x y
21 20 rexbidva x y A = z * | x z z < y y A = x y
22 21 rexbiia x y A = z * | x z z < y x y A = x y
23 8 12 22 3bitri A ran . 2 x y A = x y