# Metamath Proof Explorer

## Theorem supxrunb2

Description: The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006)

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

### Proof

Step Hyp Ref Expression
1 ssel
` |-  ( A C_ RR* -> ( z e. A -> z e. RR* ) )`
2 pnfnlt
` |-  ( z e. RR* -> -. +oo < z )`
3 1 2 syl6
` |-  ( A C_ RR* -> ( z e. A -> -. +oo < z ) )`
4 3 ralrimiv
` |-  ( A C_ RR* -> A. z e. A -. +oo < z )`
` |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A x < y ) -> A. z e. A -. +oo < z )`
6 breq1
` |-  ( x = z -> ( x < y <-> z < y ) )`
7 6 rexbidv
` |-  ( x = z -> ( E. y e. A x < y <-> E. y e. A z < y ) )`
8 7 rspcva
` |-  ( ( z e. RR /\ A. x e. RR E. y e. A x < y ) -> E. y e. A z < y )`
` |-  ( ( z e. RR /\ ( A. x e. RR E. y e. A x < y /\ A C_ RR* ) ) -> E. y e. A z < y )`
10 9 ancoms
` |-  ( ( ( A. x e. RR E. y e. A x < y /\ A C_ RR* ) /\ z e. RR ) -> E. y e. A z < y )`
11 10 exp31
` |-  ( A. x e. RR E. y e. A x < y -> ( A C_ RR* -> ( z e. RR -> E. y e. A z < y ) ) )`
12 11 a1dd
` |-  ( A. x e. RR E. y e. A x < y -> ( A C_ RR* -> ( z < +oo -> ( z e. RR -> E. y e. A z < y ) ) ) )`
13 12 com4r
` |-  ( z e. RR -> ( A. x e. RR E. y e. A x < y -> ( A C_ RR* -> ( z < +oo -> E. y e. A z < y ) ) ) )`
14 13 com13
` |-  ( A C_ RR* -> ( A. x e. RR E. y e. A x < y -> ( z e. RR -> ( z < +oo -> E. y e. A z < y ) ) ) )`
15 14 imp
` |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A x < y ) -> ( z e. RR -> ( z < +oo -> E. y e. A z < y ) ) )`
16 15 ralrimiv
` |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A x < y ) -> A. z e. RR ( z < +oo -> E. y e. A z < y ) )`
17 5 16 jca
` |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A x < y ) -> ( A. z e. A -. +oo < z /\ A. z e. RR ( z < +oo -> E. y e. A z < y ) ) )`
18 pnfxr
` |-  +oo e. RR*`
19 supxr
` |-  ( ( ( A C_ RR* /\ +oo e. RR* ) /\ ( A. z e. A -. +oo < z /\ A. z e. RR ( z < +oo -> E. y e. A z < y ) ) ) -> sup ( A , RR* , < ) = +oo )`
20 18 19 mpanl2
` |-  ( ( A C_ RR* /\ ( A. z e. A -. +oo < z /\ A. z e. RR ( z < +oo -> E. y e. A z < y ) ) ) -> sup ( A , RR* , < ) = +oo )`
21 17 20 syldan
` |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A x < y ) -> sup ( A , RR* , < ) = +oo )`
22 21 ex
` |-  ( A C_ RR* -> ( A. x e. RR E. y e. A x < y -> sup ( A , RR* , < ) = +oo ) )`
23 rexr
` |-  ( x e. RR -> x e. RR* )`
` |-  ( ( ( A C_ RR* /\ x e. RR ) /\ sup ( A , RR* , < ) = +oo ) -> x e. RR* )`
25 ltpnf
` |-  ( x e. RR -> x < +oo )`
26 breq2
` |-  ( sup ( A , RR* , < ) = +oo -> ( x < sup ( A , RR* , < ) <-> x < +oo ) )`
27 25 26 syl5ibr
` |-  ( sup ( A , RR* , < ) = +oo -> ( x e. RR -> x < sup ( A , RR* , < ) ) )`
28 27 impcom
` |-  ( ( x e. RR /\ sup ( A , RR* , < ) = +oo ) -> x < sup ( A , RR* , < ) )`
` |-  ( ( ( A C_ RR* /\ x e. RR ) /\ sup ( A , RR* , < ) = +oo ) -> x < sup ( A , RR* , < ) )`
30 xrltso
` |-  < Or RR*`
31 30 a1i
` |-  ( ( ( A C_ RR* /\ x e. RR ) /\ sup ( A , RR* , < ) = +oo ) -> < Or RR* )`
32 xrsupss
` |-  ( A C_ RR* -> E. z e. RR* ( A. w e. A -. z < w /\ A. w e. RR* ( w < z -> E. y e. A w < y ) ) )`
` |-  ( ( ( A C_ RR* /\ x e. RR ) /\ sup ( A , RR* , < ) = +oo ) -> E. z e. RR* ( A. w e. A -. z < w /\ A. w e. RR* ( w < z -> E. y e. A w < y ) ) )`
` |-  ( ( ( A C_ RR* /\ x e. RR ) /\ sup ( A , RR* , < ) = +oo ) -> ( ( x e. RR* /\ x < sup ( A , RR* , < ) ) -> E. y e. A x < y ) )`
` |-  ( ( ( A C_ RR* /\ x e. RR ) /\ sup ( A , RR* , < ) = +oo ) -> E. y e. A x < y )`
` |-  ( A C_ RR* -> ( x e. RR -> ( sup ( A , RR* , < ) = +oo -> E. y e. A x < y ) ) )`
` |-  ( A C_ RR* -> ( sup ( A , RR* , < ) = +oo -> ( x e. RR -> E. y e. A x < y ) ) )`
` |-  ( A C_ RR* -> ( sup ( A , RR* , < ) = +oo -> A. x e. RR E. y e. A x < y ) )`
` |-  ( A C_ RR* -> ( A. x e. RR E. y e. A x < y <-> sup ( A , RR* , < ) = +oo ) )`