Theorem supxrbnd2

Description: The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006)

	Ref	Expression
Assertion	supxrbnd2	|- ( A C_ RR* -> ( E. x e. RR A. y e. A y <_ x <-> sup ( A , RR* , < ) < +oo ) )

Proof

Step	Hyp	Ref	Expression
1		ralnex	|- ( A. x e. RR -. A. y e. A y <_ x <-> -. E. x e. RR A. y e. A y <_ x )
2		ssel2	|- ( ( A C_ RR* /\ y e. A ) -> y e. RR* )
3		rexr	|- ( x e. RR -> x e. RR* )
4		xrlenlt	|- ( ( y e. RR* /\ x e. RR* ) -> ( y <_ x <-> -. x < y ) )
5	4	con2bid	|- ( ( y e. RR* /\ x e. RR* ) -> ( x < y <-> -. y <_ x ) )
6	2 3 5	syl2an	|- ( ( ( A C_ RR* /\ y e. A ) /\ x e. RR ) -> ( x < y <-> -. y <_ x ) )
7	6	an32s	|- ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) -> ( x < y <-> -. y <_ x ) )
8	7	rexbidva	|- ( ( A C_ RR* /\ x e. RR ) -> ( E. y e. A x < y <-> E. y e. A -. y <_ x ) )
9		rexnal	|- ( E. y e. A -. y <_ x <-> -. A. y e. A y <_ x )
10	8 9	bitr2di	|- ( ( A C_ RR* /\ x e. RR ) -> ( -. A. y e. A y <_ x <-> E. y e. A x < y ) )
11	10	ralbidva	|- ( A C_ RR* -> ( A. x e. RR -. A. y e. A y <_ x <-> A. x e. RR E. y e. A x < y ) )
12	1 11	bitr3id	|- ( A C_ RR* -> ( -. E. x e. RR A. y e. A y <_ x <-> A. x e. RR E. y e. A x < y ) )
13		supxrunb2	|- ( A C_ RR* -> ( A. x e. RR E. y e. A x < y <-> sup ( A , RR* , < ) = +oo ) )
14		supxrcl	|- ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )
15		nltpnft	|- ( sup ( A , RR* , < ) e. RR* -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
16	14 15	syl	|- ( A C_ RR* -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
17	12 13 16	3bitrd	|- ( A C_ RR* -> ( -. E. x e. RR A. y e. A y <_ x <-> -. sup ( A , RR* , < ) < +oo ) )
18	17	con4bid	|- ( A C_ RR* -> ( E. x e. RR A. y e. A y <_ x <-> sup ( A , RR* , < ) < +oo ) )