Metamath Proof Explorer

Theorem ioopnfsup

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

Ref Expression
Assertion ioopnfsup 
|- ( ( 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 ioon0 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( ( A (,) +oo ) =/= (/) <-> A < +oo ) )
8 3 7 syldan 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> ( ( A (,) +oo ) =/= (/) <-> A < +oo ) )
9 6 8 mpbird 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> ( A (,) +oo ) =/= (/) )
10 df-ioo 
 |-  (,) = ( 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 idd 
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A < w -> A < w ) )
14 xrltle 
 |-  ( ( 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 )