Theorem iccmax

Description: The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014)

	Ref	Expression
Assertion	iccmax	|- ( -oo [,] +oo ) = RR*

Proof

Step	Hyp	Ref	Expression
1		mnfxr	|- -oo e. RR*
2		pnfxr	|- +oo e. RR*
3		iccval	|- ( ( -oo e. RR* /\ +oo e. RR* ) -> ( -oo [,] +oo ) = { x e. RR* | ( -oo <_ x /\ x <_ +oo ) } )
4	1 2 3	mp2an	|- ( -oo [,] +oo ) = { x e. RR* | ( -oo <_ x /\ x <_ +oo ) }
5		rabid2	|- ( RR* = { x e. RR* | ( -oo <_ x /\ x <_ +oo ) } <-> A. x e. RR* ( -oo <_ x /\ x <_ +oo ) )
6		mnfle	|- ( x e. RR* -> -oo <_ x )
7		pnfge	|- ( x e. RR* -> x <_ +oo )
8	6 7	jca	|- ( x e. RR* -> ( -oo <_ x /\ x <_ +oo ) )
9	5 8	mprgbir	|- RR* = { x e. RR* | ( -oo <_ x /\ x <_ +oo ) }
10	4 9	eqtr4i	|- ( -oo [,] +oo ) = RR*