Theorem supssd

Description: Inequality deduction for supremum of a subset. (Contributed by Thierry Arnoux, 21-Mar-2017)

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

Proof

Step	Hyp	Ref	Expression
1		supssd.0	|- ( ph -> R Or A )
2		supssd.1	|- ( ph -> B C_ C )
3		supssd.2	|- ( ph -> C C_ A )
4		supssd.3	|- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
5		supssd.4	|- ( ph -> E. x e. A ( A. y e. C -. x R y /\ A. y e. A ( y R x -> E. z e. C y R z ) ) )
6	1 5	supcl	|- ( ph -> sup ( C , A , R ) e. A )
7	2	sseld	|- ( ph -> ( z e. B -> z e. C ) )
8	1 5	supub	|- ( ph -> ( z e. C -> -. sup ( C , A , R ) R z ) )
9	7 8	syld	|- ( ph -> ( z e. B -> -. sup ( C , A , R ) R z ) )
10	9	ralrimiv	|- ( ph -> A. z e. B -. sup ( C , A , R ) R z )
11	1 4	supnub	|- ( ph -> ( ( sup ( C , A , R ) e. A /\ A. z e. B -. sup ( C , A , R ) R z ) -> -. sup ( C , A , R ) R sup ( B , A , R ) ) )
12	6 10 11	mp2and	|- ( ph -> -. sup ( C , A , R ) R sup ( B , A , R ) )