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