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

Metamath Proof Explorer

Theorem unirnioo

Description: The union of the range of the open interval function. (Contributed by NM, 7-May-2007) (Revised by Mario Carneiro, 30-Jan-2014)

Ref Expression
Assertion unirnioo 
|- RR = U. ran (,)

Proof

Step Hyp Ref Expression
1 ioomax 
 |-  ( -oo (,) +oo ) = RR
2 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
3 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
4 2 3 ax-mp 
 |-  (,) Fn ( RR* X. RR* )
5 mnfxr 
 |-  -oo e. RR*
6 pnfxr 
 |-  +oo e. RR*
7 fnovrn 
 |-  ( ( (,) Fn ( RR* X. RR* ) /\ -oo e. RR* /\ +oo e. RR* ) -> ( -oo (,) +oo ) e. ran (,) )
8 4 5 6 7 mp3an 
 |-  ( -oo (,) +oo ) e. ran (,)
9 1 8 eqeltrri 
 |-  RR e. ran (,)
10 elssuni 
 |-  ( RR e. ran (,) -> RR C_ U. ran (,) )
11 9 10 ax-mp 
 |-  RR C_ U. ran (,)
12 frn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> ran (,) C_ ~P RR )
13 2 12 ax-mp 
 |-  ran (,) C_ ~P RR
14 sspwuni 
 |-  ( ran (,) C_ ~P RR <-> U. ran (,) C_ RR )
15 13 14 mpbi 
 |-  U. ran (,) C_ RR
16 11 15 eqssi 
 |-  RR = U. ran (,)