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 , < ) )