This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) } )