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 (,)