Metamath Proof Explorer


Theorem supxrre

Description: The real and extended real suprema match when the real supremum exists. (Contributed by NM, 18-Oct-2005) (Proof shortened by Mario Carneiro, 7-Sep-2014)

Ref Expression
Assertion supxrre
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR* , < ) = sup ( A , RR , < ) )

Proof

Step Hyp Ref Expression
1 simp1
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> A C_ RR )
2 ressxr
 |-  RR C_ RR*
3 1 2 sstrdi
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> A C_ RR* )
4 supxrcl
 |-  ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )
5 3 4 syl
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR* , < ) e. RR* )
6 suprcl
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
7 6 rexrd
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR* )
8 6 leidd
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) <_ sup ( A , RR , < ) )
9 suprleub
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ sup ( A , RR , < ) e. RR ) -> ( sup ( A , RR , < ) <_ sup ( A , RR , < ) <-> A. z e. A z <_ sup ( A , RR , < ) ) )
10 6 9 mpdan
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> ( sup ( A , RR , < ) <_ sup ( A , RR , < ) <-> A. z e. A z <_ sup ( A , RR , < ) ) )
11 supxrleub
 |-  ( ( A C_ RR* /\ sup ( A , RR , < ) e. RR* ) -> ( sup ( A , RR* , < ) <_ sup ( A , RR , < ) <-> A. z e. A z <_ sup ( A , RR , < ) ) )
12 3 7 11 syl2anc
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> ( sup ( A , RR* , < ) <_ sup ( A , RR , < ) <-> A. z e. A z <_ sup ( A , RR , < ) ) )
13 10 12 bitr4d
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> ( sup ( A , RR , < ) <_ sup ( A , RR , < ) <-> sup ( A , RR* , < ) <_ sup ( A , RR , < ) ) )
14 8 13 mpbid
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR* , < ) <_ sup ( A , RR , < ) )
15 5 xrleidd
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR* , < ) <_ sup ( A , RR* , < ) )
16 supxrleub
 |-  ( ( A C_ RR* /\ sup ( A , RR* , < ) e. RR* ) -> ( sup ( A , RR* , < ) <_ sup ( A , RR* , < ) <-> A. x e. A x <_ sup ( A , RR* , < ) ) )
17 3 5 16 syl2anc
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> ( sup ( A , RR* , < ) <_ sup ( A , RR* , < ) <-> A. x e. A x <_ sup ( A , RR* , < ) ) )
18 simp2
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> A =/= (/) )
19 n0
 |-  ( A =/= (/) <-> E. z z e. A )
20 18 19 sylib
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> E. z z e. A )
21 mnfxr
 |-  -oo e. RR*
22 21 a1i
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ z e. A ) -> -oo e. RR* )
23 1 sselda
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ z e. A ) -> z e. RR )
24 23 rexrd
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ z e. A ) -> z e. RR* )
25 5 adantr
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ z e. A ) -> sup ( A , RR* , < ) e. RR* )
26 23 mnfltd
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ z e. A ) -> -oo < z )
27 supxrub
 |-  ( ( A C_ RR* /\ z e. A ) -> z <_ sup ( A , RR* , < ) )
28 3 27 sylan
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ z e. A ) -> z <_ sup ( A , RR* , < ) )
29 22 24 25 26 28 xrltletrd
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ z e. A ) -> -oo < sup ( A , RR* , < ) )
30 20 29 exlimddv
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> -oo < sup ( A , RR* , < ) )
31 xrre
 |-  ( ( ( sup ( A , RR* , < ) e. RR* /\ sup ( A , RR , < ) e. RR ) /\ ( -oo < sup ( A , RR* , < ) /\ sup ( A , RR* , < ) <_ sup ( A , RR , < ) ) ) -> sup ( A , RR* , < ) e. RR )
32 5 6 30 14 31 syl22anc
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR* , < ) e. RR )
33 suprleub
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ sup ( A , RR* , < ) e. RR ) -> ( sup ( A , RR , < ) <_ sup ( A , RR* , < ) <-> A. x e. A x <_ sup ( A , RR* , < ) ) )
34 32 33 mpdan
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> ( sup ( A , RR , < ) <_ sup ( A , RR* , < ) <-> A. x e. A x <_ sup ( A , RR* , < ) ) )
35 17 34 bitr4d
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> ( sup ( A , RR* , < ) <_ sup ( A , RR* , < ) <-> sup ( A , RR , < ) <_ sup ( A , RR* , < ) ) )
36 15 35 mpbid
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) <_ sup ( A , RR* , < ) )
37 5 7 14 36 xrletrid
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR* , < ) = sup ( A , RR , < ) )