# 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* )`
` |-  ( ( ( 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 , < ) )`