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 e. ran ( [,) |` ( RR X. RR ) ) <-> E. x e. RR E. y e. RR A = ( x [,) y ) )

Proof

Step Hyp Ref Expression
1 df-ico 
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
2 1 reseq1i 
 |-  ( [,) |` ( RR X. RR ) ) = ( ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } ) |` ( RR X. RR ) )
3 ressxr 
 |-  RR C_ RR*
4 resmpo 
 |-  ( ( RR C_ RR* /\ RR C_ RR* ) -> ( ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } ) |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } ) )
5 3 3 4 mp2an 
 |-  ( ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } ) |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } )
6 2 5 eqtri 
 |-  ( [,) |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } )
7 6 rneqi 
 |-  ran ( [,) |` ( RR X. RR ) ) = ran ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } )
8 7 eleq2i 
 |-  ( A e. ran ( [,) |` ( RR X. RR ) ) <-> A e. ran ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } ) )
9 eqid 
 |-  ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } ) = ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } )
10 xrex 
 |-  RR* e. _V
11 10 rabex 
 |-  { z e. RR* | ( x <_ z /\ z < y ) } e. _V
12 9 11 elrnmpo 
 |-  ( A e. ran ( x e. RR , y e. RR |-> { z e. RR* | ( x <_ z /\ z < y ) } ) <-> E. x e. RR E. y e. RR A = { z e. RR* | ( x <_ z /\ z < y ) } )
13 3 sseli 
 |-  ( x e. RR -> x e. RR* )
14 13 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> x e. RR* )
15 3 sseli 
 |-  ( y e. RR -> y e. RR* )
16 15 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> y e. RR* )
17 icoval 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x [,) y ) = { z e. RR* | ( x <_ z /\ z < y ) } )
18 14 16 17 syl2anc 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x [,) y ) = { z e. RR* | ( x <_ z /\ z < y ) } )
19 18 eqcomd 
 |-  ( ( x e. RR /\ y e. RR ) -> { z e. RR* | ( x <_ z /\ z < y ) } = ( x [,) y ) )
20 19 eqeq2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( A = { z e. RR* | ( x <_ z /\ z < y ) } <-> A = ( x [,) y ) ) )
21 20 rexbidva 
 |-  ( x e. RR -> ( E. y e. RR A = { z e. RR* | ( x <_ z /\ z < y ) } <-> E. y e. RR A = ( x [,) y ) ) )
22 21 rexbiia 
 |-  ( E. x e. RR E. y e. RR A = { z e. RR* | ( x <_ z /\ z < y ) } <-> E. x e. RR E. y e. RR A = ( x [,) y ) )
23 8 12 22 3bitri 
 |-  ( A e. ran ( [,) |` ( RR X. RR ) ) <-> E. x e. RR E. y e. RR A = ( x [,) y ) )