Theorem infnlb

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

	Ref	Expression
Hypotheses	infcl.1	$$⊢\phi \to R\mathrm{Or}A$$
	infcl.2	$$⊢\phi \to \exists x\in A\left(\forall y\in B\neg yRx\wedge \forall y\in A\left(xRy\to \exists z\in BzRy\right)\right)$$
Assertion	infnlb	$$⊢\phi \to \left(\left(C\in A\wedge \forall z\in B\neg zRC\right)\to \neg inf\left(B,A,R\right)RC\right)$$

Proof

Step	Hyp	Ref	Expression
1		infcl.1	$$⊢\phi \to R\mathrm{Or}A$$
2		infcl.2	$$⊢\phi \to \exists x\in A\left(\forall y\in B\neg yRx\wedge \forall y\in A\left(xRy\to \exists z\in BzRy\right)\right)$$
3	1 2	infglb	$$⊢\phi \to \left(\left(C\in A\wedge inf\left(B,A,R\right)RC\right)\to \exists z\in BzRC\right)$$
4	3	expdimp	$$⊢\left(\phi \wedge C\in A\right)\to \left(inf\left(B,A,R\right)RC\to \exists z\in BzRC\right)$$
5		dfrex2	$$⊢\exists z\in BzRC\leftrightarrow \neg \forall z\in B\neg zRC$$
6	4 5	imbitrdi	$$⊢\left(\phi \wedge C\in A\right)\to \left(inf\left(B,A,R\right)RC\to \neg \forall z\in B\neg zRC\right)$$
7	6	con2d	$$⊢\left(\phi \wedge C\in A\right)\to \left(\forall z\in B\neg zRC\to \neg inf\left(B,A,R\right)RC\right)$$
8	7	expimpd	$$⊢\phi \to \left(\left(C\in A\wedge \forall z\in B\neg zRC\right)\to \neg inf\left(B,A,R\right)RC\right)$$