Metamath Proof Explorer

Theorem iooval2

Description: Value of the open interval function. (Contributed by NM, 6-Feb-2007) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion iooval2 
|- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = { x e. RR | ( A < x /\ x < B ) } )

Proof

Step Hyp Ref Expression
1 iooval 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = { x e. RR* | ( A < x /\ x < B ) } )
2 elioore 
 |-  ( x e. ( A (,) B ) -> x e. RR )
3 2 ssriv 
 |-  ( A (,) B ) C_ RR
4 1 3 eqsstrrdi 
 |-  ( ( A e. RR* /\ B e. RR* ) -> { x e. RR* | ( A < x /\ x < B ) } C_ RR )
5 dfss2 
 |-  ( { x e. RR* | ( A < x /\ x < B ) } C_ RR <-> ( { x e. RR* | ( A < x /\ x < B ) } i^i RR ) = { x e. RR* | ( A < x /\ x < B ) } )
6 4 5 sylib 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( { x e. RR* | ( A < x /\ x < B ) } i^i RR ) = { x e. RR* | ( A < x /\ x < B ) } )
7 inrab2 
 |-  ( { x e. RR* | ( A < x /\ x < B ) } i^i RR ) = { x e. ( RR* i^i RR ) | ( A < x /\ x < B ) }
8 ressxr 
 |-  RR C_ RR*
9 sseqin2 
 |-  ( RR C_ RR* <-> ( RR* i^i RR ) = RR )
10 8 9 mpbi 
 |-  ( RR* i^i RR ) = RR
11 10 rabeqi 
 |-  { x e. ( RR* i^i RR ) | ( A < x /\ x < B ) } = { x e. RR | ( A < x /\ x < B ) }
12 7 11 eqtri 
 |-  ( { x e. RR* | ( A < x /\ x < B ) } i^i RR ) = { x e. RR | ( A < x /\ x < B ) }
13 6 12 eqtr3di 
 |-  ( ( A e. RR* /\ B e. RR* ) -> { x e. RR* | ( A < x /\ x < B ) } = { x e. RR | ( A < x /\ x < B ) } )
14 1 13 eqtrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = { x e. RR | ( A < x /\ x < B ) } )