This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )