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

Metamath Proof Explorer

Theorem ioomax

Description: The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007)

Ref Expression
Assertion ioomax 
|- ( -oo (,) +oo ) = RR

Proof

Step Hyp Ref Expression
1 mnfxr 
 |-  -oo e. RR*
2 pnfxr 
 |-  +oo e. RR*
3 iooval2 
 |-  ( ( -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 mnflt 
 |-  ( x e. RR -> -oo < x )
7 ltpnf 
 |-  ( 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