Metamath Proof Explorer

Theorem gtinf

Description: Any number greater than an infimum is greater than some element of the set. (Contributed by Jeff Hankins, 29-Sep-2013) (Revised by AV, 10-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. y e. S x <_ y ) /\ ( A e. RR /\ inf ( S , RR , < ) < A ) ) -> A e. RR )
2 simprr 
 |-  ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. y e. S x <_ y ) /\ ( A e. RR /\ inf ( S , RR , < ) < A ) ) -> inf ( S , RR , < ) < A )
3 ltso 
 |-  < Or RR
4 3 a1i 
 |-  ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. y e. S x <_ y ) /\ ( A e. RR /\ inf ( S , RR , < ) < A ) ) -> < Or RR )
5 infm3 
 |-  ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. y e. S x <_ y ) -> E. x e. RR ( A. y e. S -. y < x /\ A. y e. RR ( x < y -> E. z e. S z < y ) ) )
6 5 adantr 
 |-  ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. y e. S x <_ y ) /\ ( A e. RR /\ inf ( S , RR , < ) < A ) ) -> E. x e. RR ( A. y e. S -. y < x /\ A. y e. RR ( x < y -> E. z e. S z < y ) ) )
7 4 6 infglb 
 |-  ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. y e. S x <_ y ) /\ ( A e. RR /\ inf ( S , RR , < ) < A ) ) -> ( ( A e. RR /\ inf ( S , RR , < ) < A ) -> E. z e. S z < A ) )
8 1 2 7 mp2and 
 |-  ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. y e. S x <_ y ) /\ ( A e. RR /\ inf ( S , RR , < ) < A ) ) -> E. z e. S z < A )