Theorem supxrbnd1

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

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