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

Metamath Proof Explorer

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