Theorem eqinfd

Description: Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 3-Sep-2020)

	Ref	Expression
Hypotheses	infexd.1	$$⊢\phi \to R\mathrm{Or}A$$
	eqinfd.2	$$⊢\phi \to C\in A$$
	eqinfd.3	$$⊢\left(\phi \wedge y\in B\right)\to \neg yRC$$
	eqinfd.4	$$⊢\left(\phi \wedge \left(y\in A\wedge CRy\right)\right)\to \exists z\in BzRy$$
Assertion	eqinfd	$$⊢\phi \to inf\left(B,A,R\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		infexd.1	$$⊢\phi \to R\mathrm{Or}A$$
2		eqinfd.2	$$⊢\phi \to C\in A$$
3		eqinfd.3	$$⊢\left(\phi \wedge y\in B\right)\to \neg yRC$$
4		eqinfd.4	$$⊢\left(\phi \wedge \left(y\in A\wedge CRy\right)\right)\to \exists z\in BzRy$$
5	3	ralrimiva	$$⊢\phi \to \forall y\in B\neg yRC$$
6	4	expr	$$⊢\left(\phi \wedge y\in A\right)\to \left(CRy\to \exists z\in BzRy\right)$$
7	6	ralrimiva	$$⊢\phi \to \forall y\in A\left(CRy\to \exists z\in BzRy\right)$$
8	1	eqinf	$$⊢\phi \to \left(\left(C\in A\wedge \forall y\in B\neg yRC\wedge \forall y\in A\left(CRy\to \exists z\in BzRy\right)\right)\to inf\left(B,A,R\right)=C\right)$$
9	2 5 7 8	mp3and	$$⊢\phi \to inf\left(B,A,R\right)=C$$