Metamath Proof Explorer

Theorem supxrpnf

Description: The supremum of a set of extended reals containing plus infinity is plus infinity. (Contributed by NM, 15-Oct-2005)

Ref Expression
Assertion supxrpnf 
|- ( ( A C_ RR* /\ +oo e. A ) -> sup ( A , RR* , < ) = +oo )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( A C_ RR* -> ( y e. A -> y e. RR* ) )
2 pnfnlt 
 |-  ( y e. RR* -> -. +oo < y )
3 1 2 syl6 
 |-  ( A C_ RR* -> ( y e. A -> -. +oo < y ) )
4 3 ralrimiv 
 |-  ( A C_ RR* -> A. y e. A -. +oo < y )
5 breq2 
 |-  ( z = +oo -> ( y < z <-> y < +oo ) )
6 5 rspcev 
 |-  ( ( +oo e. A /\ y < +oo ) -> E. z e. A y < z )
7 6 ex 
 |-  ( +oo e. A -> ( y < +oo -> E. z e. A y < z ) )
8 7 ralrimivw 
 |-  ( +oo e. A -> A. y e. RR ( y < +oo -> E. z e. A y < z ) )
9 4 8 anim12i 
 |-  ( ( A C_ RR* /\ +oo e. A ) -> ( A. y e. A -. +oo < y /\ A. y e. RR ( y < +oo -> E. z e. A y < z ) ) )
10 pnfxr 
 |-  +oo e. RR*
11 supxr 
 |-  ( ( ( A C_ RR* /\ +oo e. RR* ) /\ ( A. y e. A -. +oo < y /\ A. y e. RR ( y < +oo -> E. z e. A y < z ) ) ) -> sup ( A , RR* , < ) = +oo )
12 10 11 mpanl2 
 |-  ( ( A C_ RR* /\ ( A. y e. A -. +oo < y /\ A. y e. RR ( y < +oo -> E. z e. A y < z ) ) ) -> sup ( A , RR* , < ) = +oo )
13 9 12 syldan 
 |-  ( ( A C_ RR* /\ +oo e. A ) -> sup ( A , RR* , < ) = +oo )