Theorem dfioo2

Description: Alternate definition of the set of open intervals of extended reals. (Contributed by NM, 1-Mar-2007) (Revised by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Assertion	dfioo2	|- (,) = ( x e. RR* , y e. RR* |-> { w e. RR | ( x < w /\ w < y ) } )

Proof

Step	Hyp	Ref	Expression
1		ioof	|- (,) : ( RR* X. RR* ) --> ~P RR
2		ffn	|- ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
3	1 2	ax-mp	|- (,) Fn ( RR* X. RR* )
4		fnov	|- ( (,) Fn ( RR* X. RR* ) <-> (,) = ( x e. RR* , y e. RR* |-> ( x (,) y ) ) )
5	3 4	mpbi	|- (,) = ( x e. RR* , y e. RR* |-> ( x (,) y ) )
6		iooval2	|- ( ( x e. RR* /\ y e. RR* ) -> ( x (,) y ) = { w e. RR | ( x < w /\ w < y ) } )
7	6	mpoeq3ia	|- ( x e. RR* , y e. RR* |-> ( x (,) y ) ) = ( x e. RR* , y e. RR* |-> { w e. RR | ( x < w /\ w < y ) } )
8	5 7	eqtri	|- (,) = ( x e. RR* , y e. RR* |-> { w e. RR | ( x < w /\ w < y ) } )