This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infnlb

Description: A lower bound is not greater than the infimum. (Contributed by AV, 3-Sep-2020)

Ref Expression
Hypotheses infcl.1 
|- ( ph -> R Or A )
infcl.2 
|- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
Assertion infnlb 
|- ( ph -> ( ( C e. A /\ A. z e. B -. z R C ) -> -. inf ( B , A , R ) R C ) )

Proof

Step Hyp Ref Expression
1 infcl.1 
 |-  ( ph -> R Or A )
2 infcl.2 
 |-  ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
3 1 2 infglb 
 |-  ( ph -> ( ( C e. A /\ inf ( B , A , R ) R C ) -> E. z e. B z R C ) )
4 3 expdimp 
 |-  ( ( ph /\ C e. A ) -> ( inf ( B , A , R ) R C -> E. z e. B z R C ) )
5 dfrex2 
 |-  ( E. z e. B z R C <-> -. A. z e. B -. z R C )
6 4 5 imbitrdi 
 |-  ( ( ph /\ C e. A ) -> ( inf ( B , A , R ) R C -> -. A. z e. B -. z R C ) )
7 6 con2d 
 |-  ( ( ph /\ C e. A ) -> ( A. z e. B -. z R C -> -. inf ( B , A , R ) R C ) )
8 7 expimpd 
 |-  ( ph -> ( ( C e. A /\ A. z e. B -. z R C ) -> -. inf ( B , A , R ) R C ) )