Metamath Proof Explorer

Theorem ioorebas

Description: Open intervals are elements of the set of all open intervals. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Assertion ioorebas 
|- ( A (,) B ) e. ran (,)

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ( A (,) B ) = (/) -> ( A (,) B ) = (/) )
2 iooid 
 |-  ( 0 (,) 0 ) = (/)
3 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
4 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
5 3 4 ax-mp 
 |-  (,) Fn ( RR* X. RR* )
6 0xr 
 |-  0 e. RR*
7 fnovrn 
 |-  ( ( (,) Fn ( RR* X. RR* ) /\ 0 e. RR* /\ 0 e. RR* ) -> ( 0 (,) 0 ) e. ran (,) )
8 5 6 6 7 mp3an 
 |-  ( 0 (,) 0 ) e. ran (,)
9 2 8 eqeltrri 
 |-  (/) e. ran (,)
10 1 9 eqeltrdi 
 |-  ( ( A (,) B ) = (/) -> ( A (,) B ) e. ran (,) )
11 n0 
 |-  ( ( A (,) B ) =/= (/) <-> E. x x e. ( A (,) B ) )
12 eliooxr 
 |-  ( x e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* ) )
13 fnovrn 
 |-  ( ( (,) Fn ( RR* X. RR* ) /\ A e. RR* /\ B e. RR* ) -> ( A (,) B ) e. ran (,) )
14 5 13 mp3an1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) e. ran (,) )
15 12 14 syl 
 |-  ( x e. ( A (,) B ) -> ( A (,) B ) e. ran (,) )
16 15 exlimiv 
 |-  ( E. x x e. ( A (,) B ) -> ( A (,) B ) e. ran (,) )
17 11 16 sylbi 
 |-  ( ( A (,) B ) =/= (/) -> ( A (,) B ) e. ran (,) )
18 10 17 pm2.61ine 
 |-  ( A (,) B ) e. ran (,)