Theorem infmin

Description: The smallest element of a set is its infimum. Note that the converse is not true; the infimum might not be an element of the set considered. (Contributed by AV, 3-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		infmin.1	$$⊢\phi \to R\mathrm{Or}A$$
2		infmin.2	$$⊢\phi \to C\in A$$
3		infmin.3	$$⊢\phi \to C\in B$$
4		infmin.4	$$⊢\left(\phi \wedge y\in B\right)\to \neg yRC$$
5		simprr	$$⊢\left(\phi \wedge \left(y\in A\wedge CRy\right)\right)\to CRy$$
6		breq1	$$⊢z=C\to \left(zRy\leftrightarrow CRy\right)$$
7	6	rspcev	$$⊢\left(C\in B\wedge CRy\right)\to \exists z\in BzRy$$
8	3 5 7	syl2an2r	$$⊢\left(\phi \wedge \left(y\in A\wedge CRy\right)\right)\to \exists z\in BzRy$$
9	1 2 4 8	eqinfd	$$⊢\phi \to inf\left(B,A,R\right)=C$$