Metamath Proof Explorer

Theorem infrelb

Description: If a nonempty set of real numbers has a lower bound, its infimum is less than or equal to any of its elements. (Contributed by Jeff Hankins, 15-Sep-2013) (Revised by AV, 4-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y /\ A e. B ) -> B C_ RR )
2 ne0i 
 |-  ( A e. B -> B =/= (/) )
3 2 3ad2ant3 
 |-  ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y /\ A e. B ) -> B =/= (/) )
4 simp2 
 |-  ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y /\ A e. B ) -> E. x e. RR A. y e. B x <_ y )
5 infrecl 
 |-  ( ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B x <_ y ) -> inf ( B , RR , < ) e. RR )
6 1 3 4 5 syl3anc 
 |-  ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y /\ A e. B ) -> inf ( B , RR , < ) e. RR )
7 ssel2 
 |-  ( ( B C_ RR /\ A e. B ) -> A e. RR )
8 7 3adant2 
 |-  ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y /\ A e. B ) -> A e. RR )
9 ltso 
 |-  < Or RR
10 9 a1i 
 |-  ( ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y ) /\ A e. B ) -> < Or RR )
11 simpll 
 |-  ( ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y ) /\ A e. B ) -> B C_ RR )
12 2 adantl 
 |-  ( ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y ) /\ A e. B ) -> B =/= (/) )
13 simplr 
 |-  ( ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y ) /\ A e. B ) -> E. x e. RR A. y e. B x <_ y )
14 infm3 
 |-  ( ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B x <_ y ) -> E. x e. RR ( A. y e. B -. y < x /\ A. y e. RR ( x < y -> E. z e. B z < y ) ) )
15 11 12 13 14 syl3anc 
 |-  ( ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y ) /\ A e. B ) -> E. x e. RR ( A. y e. B -. y < x /\ A. y e. RR ( x < y -> E. z e. B z < y ) ) )
16 10 15 inflb 
 |-  ( ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y ) /\ A e. B ) -> ( A e. B -> -. A < inf ( B , RR , < ) ) )
17 16 expcom 
 |-  ( A e. B -> ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y ) -> ( A e. B -> -. A < inf ( B , RR , < ) ) ) )
18 17 pm2.43b 
 |-  ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y ) -> ( A e. B -> -. A < inf ( B , RR , < ) ) )
19 18 3impia 
 |-  ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y /\ A e. B ) -> -. A < inf ( B , RR , < ) )
20 6 8 19 nltled 
 |-  ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y /\ A e. B ) -> inf ( B , RR , < ) <_ A )