Metamath Proof Explorer

Theorem supxrunb1

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

Ref Expression
Assertion supxrunb1 
|- ( 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 peano2re 
 |-  ( z e. RR -> ( z + 1 ) e. RR )
7 breq1 
 |-  ( x = ( z + 1 ) -> ( x <_ y <-> ( z + 1 ) <_ y ) )
8 7 rexbidv 
 |-  ( x = ( z + 1 ) -> ( E. y e. A x <_ y <-> E. y e. A ( z + 1 ) <_ y ) )
9 8 rspcva 
 |-  ( ( ( z + 1 ) e. RR /\ A. x e. RR E. y e. A x <_ y ) -> E. y e. A ( z + 1 ) <_ y )
10 9 adantrr 
 |-  ( ( ( z + 1 ) e. RR /\ ( A. x e. RR E. y e. A x <_ y /\ A C_ RR* ) ) -> E. y e. A ( z + 1 ) <_ y )
11 10 ancoms 
 |-  ( ( ( A. x e. RR E. y e. A x <_ y /\ A C_ RR* ) /\ ( z + 1 ) e. RR ) -> E. y e. A ( z + 1 ) <_ y )
12 6 11 sylan2 
 |-  ( ( ( A. x e. RR E. y e. A x <_ y /\ A C_ RR* ) /\ z e. RR ) -> E. y e. A ( z + 1 ) <_ y )
13 ssel2 
 |-  ( ( A C_ RR* /\ y e. A ) -> y e. RR* )
14 ltp1 
 |-  ( z e. RR -> z < ( z + 1 ) )
15 14 adantr 
 |-  ( ( z e. RR /\ y e. RR* ) -> z < ( z + 1 ) )
16 6 ancli 
 |-  ( z e. RR -> ( z e. RR /\ ( z + 1 ) e. RR ) )
17 rexr 
 |-  ( z e. RR -> z e. RR* )
18 rexr 
 |-  ( ( z + 1 ) e. RR -> ( z + 1 ) e. RR* )
19 xrltletr 
 |-  ( ( z e. RR* /\ ( z + 1 ) e. RR* /\ y e. RR* ) -> ( ( z < ( z + 1 ) /\ ( z + 1 ) <_ y ) -> z < y ) )
20 18 19 syl3an2 
 |-  ( ( z e. RR* /\ ( z + 1 ) e. RR /\ y e. RR* ) -> ( ( z < ( z + 1 ) /\ ( z + 1 ) <_ y ) -> z < y ) )
21 17 20 syl3an1 
 |-  ( ( z e. RR /\ ( z + 1 ) e. RR /\ y e. RR* ) -> ( ( z < ( z + 1 ) /\ ( z + 1 ) <_ y ) -> z < y ) )
22 21 3expa 
 |-  ( ( ( z e. RR /\ ( z + 1 ) e. RR ) /\ y e. RR* ) -> ( ( z < ( z + 1 ) /\ ( z + 1 ) <_ y ) -> z < y ) )
23 16 22 sylan 
 |-  ( ( z e. RR /\ y e. RR* ) -> ( ( z < ( z + 1 ) /\ ( z + 1 ) <_ y ) -> z < y ) )
24 15 23 mpand 
 |-  ( ( z e. RR /\ y e. RR* ) -> ( ( z + 1 ) <_ y -> z < y ) )
25 24 ancoms 
 |-  ( ( y e. RR* /\ z e. RR ) -> ( ( z + 1 ) <_ y -> z < y ) )
26 13 25 sylan 
 |-  ( ( ( A C_ RR* /\ y e. A ) /\ z e. RR ) -> ( ( z + 1 ) <_ y -> z < y ) )
27 26 an32s 
 |-  ( ( ( A C_ RR* /\ z e. RR ) /\ y e. A ) -> ( ( z + 1 ) <_ y -> z < y ) )
28 27 reximdva 
 |-  ( ( A C_ RR* /\ z e. RR ) -> ( E. y e. A ( z + 1 ) <_ y -> E. y e. A z < y ) )
29 28 adantll 
 |-  ( ( ( A. x e. RR E. y e. A x <_ y /\ A C_ RR* ) /\ z e. RR ) -> ( E. y e. A ( z + 1 ) <_ y -> E. y e. A z < y ) )
30 12 29 mpd 
 |-  ( ( ( A. x e. RR E. y e. A x <_ y /\ A C_ RR* ) /\ z e. RR ) -> E. y e. A z < y )
31 30 exp31 
 |-  ( A. x e. RR E. y e. A x <_ y -> ( A C_ RR* -> ( z e. RR -> E. y e. A z < y ) ) )
32 31 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 ) ) ) )
33 32 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 ) ) ) )
34 33 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 ) ) ) )
35 34 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 ) ) )
36 35 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 ) )
37 5 36 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 ) ) )
38 pnfxr 
 |-  +oo e. RR*
39 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 )
40 38 39 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 )
41 37 40 syldan 
 |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A x <_ y ) -> sup ( A , RR* , < ) = +oo )
42 41 ex 
 |-  ( A C_ RR* -> ( A. x e. RR E. y e. A x <_ y -> sup ( A , RR* , < ) = +oo ) )
43 rexr 
 |-  ( x e. RR -> x e. RR* )
44 43 ad2antlr 
 |-  ( ( ( A C_ RR* /\ x e. RR ) /\ sup ( A , RR* , < ) = +oo ) -> x e. RR* )
45 ltpnf 
 |-  ( x e. RR -> x < +oo )
46 breq2 
 |-  ( sup ( A , RR* , < ) = +oo -> ( x < sup ( A , RR* , < ) <-> x < +oo ) )
47 45 46 imbitrrid 
 |-  ( sup ( A , RR* , < ) = +oo -> ( x e. RR -> x < sup ( A , RR* , < ) ) )
48 47 impcom 
 |-  ( ( x e. RR /\ sup ( A , RR* , < ) = +oo ) -> x < sup ( A , RR* , < ) )
49 48 adantll 
 |-  ( ( ( A C_ RR* /\ x e. RR ) /\ sup ( A , RR* , < ) = +oo ) -> x < sup ( A , RR* , < ) )
50 xrltso 
 |-  < Or RR*
51 50 a1i 
 |-  ( ( ( A C_ RR* /\ x e. RR ) /\ sup ( A , RR* , < ) = +oo ) -> < Or RR* )
52 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 ) ) )
53 52 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 ) ) )
54 51 53 suplub 
 |-  ( ( ( A C_ RR* /\ x e. RR ) /\ sup ( A , RR* , < ) = +oo ) -> ( ( x e. RR* /\ x < sup ( A , RR* , < ) ) -> E. y e. A x < y ) )
55 44 49 54 mp2and 
 |-  ( ( ( A C_ RR* /\ x e. RR ) /\ sup ( A , RR* , < ) = +oo ) -> E. y e. A x < y )
56 55 ex 
 |-  ( ( A C_ RR* /\ x e. RR ) -> ( sup ( A , RR* , < ) = +oo -> E. y e. A x < y ) )
57 43 ad2antlr 
 |-  ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) -> x e. RR* )
58 13 adantlr 
 |-  ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) -> y e. RR* )
59 xrltle 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x < y -> x <_ y ) )
60 57 58 59 syl2anc 
 |-  ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) -> ( x < y -> x <_ y ) )
61 60 reximdva 
 |-  ( ( A C_ RR* /\ x e. RR ) -> ( E. y e. A x < y -> E. y e. A x <_ y ) )
62 56 61 syld 
 |-  ( ( A C_ RR* /\ x e. RR ) -> ( sup ( A , RR* , < ) = +oo -> E. y e. A x <_ y ) )
63 62 ralrimdva 
 |-  ( A C_ RR* -> ( sup ( A , RR* , < ) = +oo -> A. x e. RR E. y e. A x <_ y ) )
64 42 63 impbid 
 |-  ( A C_ RR* -> ( A. x e. RR E. y e. A x <_ y <-> sup ( A , RR* , < ) = +oo ) )