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	|- ( ph -> R Or A )
	infmin.2	|- ( ph -> C e. A )
	infmin.3	|- ( ph -> C e. B )
	infmin.4	|- ( ( ph /\ y e. B ) -> -. y R C )
Assertion	infmin	|- ( ph -> inf ( B , A , R ) = C )

Proof

Step	Hyp	Ref	Expression
1		infmin.1	|- ( ph -> R Or A )
2		infmin.2	|- ( ph -> C e. A )
3		infmin.3	|- ( ph -> C e. B )
4		infmin.4	|- ( ( ph /\ y e. B ) -> -. y R C )
5		simprr	|- ( ( ph /\ ( y e. A /\ C R y ) ) -> C R y )
6		breq1	|- ( z = C -> ( z R y <-> C R y ) )
7	6	rspcev	|- ( ( C e. B /\ C R y ) -> E. z e. B z R y )
8	3 5 7	syl2an2r	|- ( ( ph /\ ( y e. A /\ C R y ) ) -> E. z e. B z R y )
9	1 2 4 8	eqinfd	|- ( ph -> inf ( B , A , R ) = C )