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	syl6ib	|- ( ( 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 ) )