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