Theorem infcl

Description: An infimum belongs to its base class (closure law). See also inflb and infglb . (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	infcl	$$⊢\phi \to inf\left(B,A,R\right)\in A$$

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	$$⊢inf\left(B,A,R\right)=sup\left(B,A,R^{-1}\right)$$
4		cnvso	$$⊢R\mathrm{Or}A\leftrightarrow R^{-1}\mathrm{Or}A$$
5	1 4	sylib	$$⊢\phi \to R^{-1}\mathrm{Or}A$$
6	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)$$
7	5 6	supcl	$$⊢\phi \to sup\left(B,A,R^{-1}\right)\in A$$
8	3 7	eqeltrid	$$⊢\phi \to inf\left(B,A,R\right)\in A$$