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 )
5 4 adantr 
 |-  ( ( 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 )
9 8 adantrr 
 |-  ( ( 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* )
24 23 ad2antlr 
 |-  ( ( ( 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* , < ) )
29 28 adantll 
 |-  ( ( ( 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 ) ) )
33 32 ad2antrr 
 |-  ( ( ( 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 ) ) )
34 31 33 suplub 
 |-  ( ( ( A C_ RR* /\ x e. RR ) /\ sup ( A , RR* , < ) = +oo ) -> ( ( x e. RR* /\ x < sup ( A , RR* , < ) ) -> E. y e. A x < y ) )
35 24 29 34 mp2and 
 |-  ( ( ( A C_ RR* /\ x e. RR ) /\ sup ( A , RR* , < ) = +oo ) -> E. y e. A x < y )
36 35 exp31 
 |-  ( A C_ RR* -> ( x e. RR -> ( sup ( A , RR* , < ) = +oo -> E. y e. A x < y ) ) )
37 36 com23 
 |-  ( A C_ RR* -> ( sup ( A , RR* , < ) = +oo -> ( x e. RR -> E. y e. A x < y ) ) )
38 37 ralrimdv 
 |-  ( A C_ RR* -> ( sup ( A , RR* , < ) = +oo -> A. x e. RR E. y e. A x < y ) )
39 22 38 impbid 
 |-  ( A C_ RR* -> ( A. x e. RR E. y e. A x < y <-> sup ( A , RR* , < ) = +oo ) )