Metamath Proof Explorer

Theorem icoreval

Description: Value of the closed-below, open-above interval function on reals. (Contributed by ML, 26-Jul-2020)

Ref Expression
Assertion icoreval 
|- ( ( A e. RR /\ B e. RR ) -> ( A [,) B ) = { z e. RR | ( A <_ z /\ z < B ) } )

Proof

Step Hyp Ref Expression
1 ovres 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A ( [,) |` ( RR X. RR ) ) B ) = ( A [,) B ) )
2 breq1 
 |-  ( x = A -> ( x <_ z <-> A <_ z ) )
3 2 anbi1d 
 |-  ( x = A -> ( ( x <_ z /\ z < y ) <-> ( A <_ z /\ z < y ) ) )
4 3 rabbidv 
 |-  ( x = A -> { z e. RR | ( x <_ z /\ z < y ) } = { z e. RR | ( A <_ z /\ z < y ) } )
5 breq2 
 |-  ( y = B -> ( z < y <-> z < B ) )
6 5 anbi2d 
 |-  ( y = B -> ( ( A <_ z /\ z < y ) <-> ( A <_ z /\ z < B ) ) )
7 6 rabbidv 
 |-  ( y = B -> { z e. RR | ( A <_ z /\ z < y ) } = { z e. RR | ( A <_ z /\ z < B ) } )
8 eqid 
 |-  ( [,) |` ( RR X. RR ) ) = ( [,) |` ( RR X. RR ) )
9 8 icorempo 
 |-  ( [,) |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> { z e. RR | ( x <_ z /\ z < y ) } )
10 reex 
 |-  RR e. _V
11 10 rabex 
 |-  { z e. RR | ( A <_ z /\ z < B ) } e. _V
12 4 7 9 11 ovmpo 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A ( [,) |` ( RR X. RR ) ) B ) = { z e. RR | ( A <_ z /\ z < B ) } )
13 1 12 eqtr3d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,) B ) = { z e. RR | ( A <_ z /\ z < B ) } )