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

Metamath Proof Explorer

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*