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		inrab2	|- ( { x e. RR* | ( A < x /\ x < B ) } i^i RR ) = { x e. ( RR* i^i RR ) | ( A < x /\ x < B ) }
3		ressxr	|- RR C_ RR*
4		sseqin2	|- ( RR C_ RR* <-> ( RR* i^i RR ) = RR )
5	3 4	mpbi	|- ( RR* i^i RR ) = RR
6	5	rabeqi	|- { x e. ( RR* i^i RR ) | ( A < x /\ x < B ) } = { x e. RR | ( A < x /\ x < B ) }
7	2 6	eqtri	|- ( { x e. RR* | ( A < x /\ x < B ) } i^i RR ) = { x e. RR | ( A < x /\ x < B ) }
8		elioore	|- ( x e. ( A (,) B ) -> x e. RR )
9	8	ssriv	|- ( A (,) B ) C_ RR
10	1 9	eqsstrrdi	|- ( ( A e. RR* /\ B e. RR* ) -> { x e. RR* | ( A < x /\ x < B ) } C_ RR )
11		df-ss	|- ( { 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 ) } )
12	10 11	sylib	|- ( ( A e. RR* /\ B e. RR* ) -> ( { x e. RR* | ( A < x /\ x < B ) } i^i RR ) = { x e. RR* | ( A < x /\ x < B ) } )
13	7 12	syl5reqr	|- ( ( 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 ) } )