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

Metamath Proof Explorer

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 ) )