Metamath Proof Explorer

Theorem infxrre

Description: The real and extended real infima match when the real infimum exists. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 5-Sep-2020)

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

Proof

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