Metamath Proof Explorer

Theorem icopnfsup

Description: An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> A e. RR* )
2 pnfxr 
 |-  +oo e. RR*
3 2 a1i 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> +oo e. RR* )
4 nltpnft 
 |-  ( A e. RR* -> ( A = +oo <-> -. A < +oo ) )
5 4 necon2abid 
 |-  ( A e. RR* -> ( A < +oo <-> A =/= +oo ) )
6 5 biimpar 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> A < +oo )
7 lbico1 
 |-  ( ( A e. RR* /\ +oo e. RR* /\ A < +oo ) -> A e. ( A [,) +oo ) )
8 1 3 6 7 syl3anc 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> A e. ( A [,) +oo ) )
9 8 ne0d 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> ( A [,) +oo ) =/= (/) )
10 df-ico 
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
11 idd 
 |-  ( ( w e. RR* /\ +oo e. RR* ) -> ( w < +oo -> w < +oo ) )
12 xrltle 
 |-  ( ( w e. RR* /\ +oo e. RR* ) -> ( w < +oo -> w <_ +oo ) )
13 xrltle 
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A < w -> A <_ w ) )
14 idd 
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A <_ w -> A <_ w ) )
15 10 11 12 13 14 ixxub 
 |-  ( ( A e. RR* /\ +oo e. RR* /\ ( A [,) +oo ) =/= (/) ) -> sup ( ( A [,) +oo ) , RR* , < ) = +oo )
16 1 3 9 15 syl3anc 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> sup ( ( A [,) +oo ) , RR* , < ) = +oo )