Theorem infglb

Description: An infimum is the greatest lower bound. See also infcl and inflb . (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	infglb	$$⊢\phi \to \left(\left(C\in A\wedge sup\left(B,A,R\right)RC\right)\to \exists z\in BzRC\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		df-inf	$$⊢sup\left(B,A,R\right)=sup\left(B,A,R^{-1}\right)$$
4	3	breq1i	$$⊢sup\left(B,A,R\right)RC\leftrightarrow sup\left(B,A,R^{-1}\right)RC$$
5		simpr	$$⊢\left(\phi \wedge C\in A\right)\to C\in A$$
6		cnvso	$$⊢R\mathrm{Or}A\leftrightarrow R^{-1}\mathrm{Or}A$$
7	1 6	sylib	$$⊢\phi \to R^{-1}\mathrm{Or}A$$
8	1 2	infcllem	$$⊢\phi \to \exists x\in A\left(\forall y\in B\neg x{R}^{-1}y\wedge \forall y\in A\left(y{R}^{-1}x\to \exists z\in By{R}^{-1}z\right)\right)$$
9	7 8	supcl	$$⊢\phi \to sup\left(B,A,R^{-1}\right)\in A$$
10	9	adantr	$$⊢\left(\phi \wedge C\in A\right)\to sup\left(B,A,R^{-1}\right)\in A$$
11		brcnvg	$$⊢\left(C\in A\wedge sup\left(B,A,R^{-1}\right)\in A\right)\to \left(C{R}^{-1}sup\left(B,A,R^{-1}\right)\leftrightarrow sup\left(B,A,R^{-1}\right)RC\right)$$
12	11	bicomd	$$⊢\left(C\in A\wedge sup\left(B,A,R^{-1}\right)\in A\right)\to \left(sup\left(B,A,R^{-1}\right)RC\leftrightarrow C{R}^{-1}sup\left(B,A,R^{-1}\right)\right)$$
13	5 10 12	syl2anc	$$⊢\left(\phi \wedge C\in A\right)\to \left(sup\left(B,A,R^{-1}\right)RC\leftrightarrow C{R}^{-1}sup\left(B,A,R^{-1}\right)\right)$$
14	4 13	bitrid	$$⊢\left(\phi \wedge C\in A\right)\to \left(sup\left(B,A,R\right)RC\leftrightarrow C{R}^{-1}sup\left(B,A,R^{-1}\right)\right)$$
15	7 8	suplub	$$⊢\phi \to \left(\left(C\in A\wedge C{R}^{-1}sup\left(B,A,R^{-1}\right)\right)\to \exists z\in BC{R}^{-1}z\right)$$
16	15	expdimp	$$⊢\left(\phi \wedge C\in A\right)\to \left(C{R}^{-1}sup\left(B,A,R^{-1}\right)\to \exists z\in BC{R}^{-1}z\right)$$
17		vex	$$⊢z\in \mathrm{V}$$
18		brcnvg	$$⊢\left(C\in A\wedge z\in \mathrm{V}\right)\to \left(C{R}^{-1}z\leftrightarrow zRC\right)$$
19	5 17 18	sylancl	$$⊢\left(\phi \wedge C\in A\right)\to \left(C{R}^{-1}z\leftrightarrow zRC\right)$$
20	19	rexbidv	$$⊢\left(\phi \wedge C\in A\right)\to \left(\exists z\in BC{R}^{-1}z\leftrightarrow \exists z\in BzRC\right)$$
21	16 20	sylibd	$$⊢\left(\phi \wedge C\in A\right)\to \left(C{R}^{-1}sup\left(B,A,R^{-1}\right)\to \exists z\in BzRC\right)$$
22	14 21	sylbid	$$⊢\left(\phi \wedge C\in A\right)\to \left(sup\left(B,A,R\right)RC\to \exists z\in BzRC\right)$$
23	22	expimpd	$$⊢\phi \to \left(\left(C\in A\wedge sup\left(B,A,R\right)RC\right)\to \exists z\in BzRC\right)$$