Metamath Proof Explorer

Theorem icoreelrnab

Description: Elementhood in the set of closed-below, open-above intervals of reals. (Contributed by ML, 27-Jul-2020)

Ref Expression
Hypothesis icoreelrnab.1 
|- I = ( [,) " ( RR X. RR ) )
Assertion icoreelrnab 
|- ( X e. I <-> E. a e. RR E. b e. RR X = { z e. RR | ( a <_ z /\ z < b ) } )

Proof

Step Hyp Ref Expression
1 icoreelrnab.1 
 |-  I = ( [,) " ( RR X. RR ) )
2 df-ima 
 |-  ( [,) " ( RR X. RR ) ) = ran ( [,) |` ( RR X. RR ) )
3 1 2 eqtri 
 |-  I = ran ( [,) |` ( RR X. RR ) )
4 3 eleq2i 
 |-  ( X e. I <-> X e. ran ( [,) |` ( RR X. RR ) ) )
5 icoreresf 
 |-  ( [,) |` ( RR X. RR ) ) : ( RR X. RR ) --> ~P RR
6 ffn 
 |-  ( ( [,) |` ( RR X. RR ) ) : ( RR X. RR ) --> ~P RR -> ( [,) |` ( RR X. RR ) ) Fn ( RR X. RR ) )
7 ovelrn 
 |-  ( ( [,) |` ( RR X. RR ) ) Fn ( RR X. RR ) -> ( X e. ran ( [,) |` ( RR X. RR ) ) <-> E. a e. RR E. b e. RR X = ( a ( [,) |` ( RR X. RR ) ) b ) ) )
8 5 6 7 mp2b 
 |-  ( X e. ran ( [,) |` ( RR X. RR ) ) <-> E. a e. RR E. b e. RR X = ( a ( [,) |` ( RR X. RR ) ) b ) )
9 4 8 bitri 
 |-  ( X e. I <-> E. a e. RR E. b e. RR X = ( a ( [,) |` ( RR X. RR ) ) b ) )
10 ovres 
 |-  ( ( a e. RR /\ b e. RR ) -> ( a ( [,) |` ( RR X. RR ) ) b ) = ( a [,) b ) )
11 10 eqeq2d 
 |-  ( ( a e. RR /\ b e. RR ) -> ( X = ( a ( [,) |` ( RR X. RR ) ) b ) <-> X = ( a [,) b ) ) )
12 11 2rexbiia 
 |-  ( E. a e. RR E. b e. RR X = ( a ( [,) |` ( RR X. RR ) ) b ) <-> E. a e. RR E. b e. RR X = ( a [,) b ) )
13 9 12 bitri 
 |-  ( X e. I <-> E. a e. RR E. b e. RR X = ( a [,) b ) )
14 icoreval 
 |-  ( ( a e. RR /\ b e. RR ) -> ( a [,) b ) = { z e. RR | ( a <_ z /\ z < b ) } )
15 14 eqeq2d 
 |-  ( ( a e. RR /\ b e. RR ) -> ( X = ( a [,) b ) <-> X = { z e. RR | ( a <_ z /\ z < b ) } ) )
16 15 2rexbiia 
 |-  ( E. a e. RR E. b e. RR X = ( a [,) b ) <-> E. a e. RR E. b e. RR X = { z e. RR | ( a <_ z /\ z < b ) } )
17 13 16 bitri 
 |-  ( X e. I <-> E. a e. RR E. b e. RR X = { z e. RR | ( a <_ z /\ z < b ) } )