Theorem infssd

Description: Inequality deduction for infimum of a subset. (Contributed by AV, 4-Oct-2020)

	Ref	Expression
Hypotheses	infssd.0	|- ( ph -> R Or A )
	infssd.1	|- ( ph -> C C_ B )
	infssd.3	|- ( ph -> E. x e. A ( A. y e. C -. y R x /\ A. y e. A ( x R y -> E. z e. C z R y ) ) )
	infssd.4	|- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
Assertion	infssd	|- ( ph -> -. inf ( C , A , R ) R inf ( B , A , R ) )

Proof

Step	Hyp	Ref	Expression
1		infssd.0	|- ( ph -> R Or A )
2		infssd.1	|- ( ph -> C C_ B )
3		infssd.3	|- ( ph -> E. x e. A ( A. y e. C -. y R x /\ A. y e. A ( x R y -> E. z e. C z R y ) ) )
4		infssd.4	|- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
5	1 4	infcl	|- ( ph -> inf ( B , A , R ) e. A )
6	2	sseld	|- ( ph -> ( z e. C -> z e. B ) )
7	1 4	inflb	|- ( ph -> ( z e. B -> -. z R inf ( B , A , R ) ) )
8	6 7	syld	|- ( ph -> ( z e. C -> -. z R inf ( B , A , R ) ) )
9	8	ralrimiv	|- ( ph -> A. z e. C -. z R inf ( B , A , R ) )
10	1 3	infnlb	|- ( ph -> ( ( inf ( B , A , R ) e. A /\ A. z e. C -. z R inf ( B , A , R ) ) -> -. inf ( C , A , R ) R inf ( B , A , R ) ) )
11	5 9 10	mp2and	|- ( ph -> -. inf ( C , A , R ) R inf ( B , A , R ) )