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 φ R Or A
infcl.2 φ x A y B ¬ y R x y A x R y z B z R y
Assertion infnlb φ C A z B ¬ z R C ¬ sup B A R R C

Proof

Step Hyp Ref Expression
1 infcl.1 φ R Or A
2 infcl.2 φ x A y B ¬ y R x y A x R y z B z R y
3 1 2 infglb φ C A sup B A R R C z B z R C
4 3 expdimp φ C A sup B A R R C z B z R C
5 dfrex2 z B z R C ¬ z B ¬ z R C
6 4 5 syl6ib φ C A sup B A R R C ¬ z B ¬ z R C
7 6 con2d φ C A z B ¬ z R C ¬ sup B A R R C
8 7 expimpd φ C A z B ¬ z R C ¬ sup B A R R C