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

Metamath Proof Explorer

Theorem xrsup0

Description: The supremum of an empty set under the extended reals is minus infinity. (Contributed by NM, 15-Oct-2005)

Ref Expression
Assertion xrsup0 
|- sup ( (/) , RR* , < ) = -oo

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ RR*
2 mnfxr 
 |-  -oo e. RR*
3 ral0 
 |-  A. y e. (/) -. -oo < y
4 rexr 
 |-  ( y e. RR -> y e. RR* )
5 nltmnf 
 |-  ( y e. RR* -> -. y < -oo )
6 4 5 syl 
 |-  ( y e. RR -> -. y < -oo )
7 6 pm2.21d 
 |-  ( y e. RR -> ( y < -oo -> E. z e. (/) y < z ) )
8 7 rgen 
 |-  A. y e. RR ( y < -oo -> E. z e. (/) y < z )
9 supxr 
 |-  ( ( ( (/) C_ RR* /\ -oo e. RR* ) /\ ( A. y e. (/) -. -oo < y /\ A. y e. RR ( y < -oo -> E. z e. (/) y < z ) ) ) -> sup ( (/) , RR* , < ) = -oo )
10 1 2 3 8 9 mp4an 
 |-  sup ( (/) , RR* , < ) = -oo