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

Proof

Step	Hyp	Ref	Expression
1		infexd.1	|- ( ph -> R Or A )
2		eqinfd.2	|- ( ph -> C e. A )
3		eqinfd.3	|- ( ( ph /\ y e. B ) -> -. y R C )
4		eqinfd.4	|- ( ( ph /\ ( y e. A /\ C R y ) ) -> E. z e. B z R y )
5	3	ralrimiva	|- ( ph -> A. y e. B -. y R C )
6	4	expr	|- ( ( ph /\ y e. A ) -> ( C R y -> E. z e. B z R y ) )
7	6	ralrimiva	|- ( ph -> A. y e. A ( C R y -> E. z e. B z R y ) )
8	1	eqinf	|- ( ph -> ( ( C e. A /\ A. y e. B -. y R C /\ A. y e. A ( C R y -> E. z e. B z R y ) ) -> inf ( B , A , R ) = C ) )
9	2 5 7 8	mp3and	|- ( ph -> inf ( B , A , R ) = C )