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

Metamath Proof Explorer

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